Formal Reasoning vs. Informal Reasoning

From Geb

"I would have preferred to show how to derive Euclid's Theorem (the infinitude of primes) in TNT, but it would probably have doubled the length of this book."

In fact, the infinitude of primes can be proved in <2000 lines of TNT. Since page 226 (20th ann. ed.) contains 28 lines of TNT, it's reasonable to assume that the proof could be included in a 71-page appendix, which would increase the book's size by less than 10%.

---

Might we use Prolog to find the shortest proof?