Cody challenged me to prove that there are an infinitely many primes in Knuckledragger, saying it’s the minimum thing to do to demonstrate you have a proof assistant. https://en.wikipedia.org/wiki/Euclid%27s_theorem It’s one of the older proofs out there, appearing famously in Euclid’s elements. This is number 11 in the formalizing 100 theorems list https://www.cs.ru.nl/~freek/100/ . Maybe it’d be fun to start chasing down the other easy ones and copy them out of Isabelle or whatever
