Hypothesis: an LLM capable of generating a correct proof in a formal language, not through random chance but through whatever passes for “reasoning,” should also be capable of describing the proof in a way meaningful to humans. Because LLMs have a limited context window and are trained on human behavior, they will generate solutions similar to what humans would generate.

We have already accepted some proofs we cannot fully understand, such as the proof of the four color theorem that used computational methods to explore a large solution space and demonstrate that no possible special-case combinations violate the theorem. But that was just one part of the proof.

I wonder what we know about proof space generally, and if we had an ASI that reasoned in a substantially different way than humans, what types of proofs it would be likely to generate. Do most proofs contain structural components that humans find pleasing? Do most devolve into convoluted case analyses? Is there a simplest form that a set of correct proofs could be reduced to?