>> In a way, yes. You can easily write a program that recursively enumerates all provable theorems in some order. But if you want a proof of a specific theorem, how do you find it in the list? You need to encode the theorem in a formal syntax first, and since mathematics is built on towers of definitions referencing other definitions, that alone is a significant amount of work before you can even write down what you want to prove.

My current framing of this is that the advantage of LLMs lies in their ability to generate the text of a proof without having derived each of its steps in order, like a theorem prover (automated or not) would have to. There's nothing forcing an LLM to derive conclusions from premises (or indeed making it at all capable to do that).

They don't have to understand what the proof they generate means, or to be able to tell whether it's true. In fact, they can't do either. But that's fine as long as it's possible to check the proof with an external verifier.

So most LLM-based proofs use the LLM as the generator and an external verifier as the tester, either a solver like Lean or a mathematician. That's the best of both worlds as far as generate-and-test goes. A powerful generator tied to a powerful tester.

EDIT: yeah, like this:

>> An example of a good division of labor is the SAT Attack on Tarski's High School Algebra Problem https://arxiv.org/abs/2608.08421 where they construct a formula with O(n⁴) variables and O(n⁶) clauses and use a SAT solver to show that it is unsatisfiable for n ≤ 11 but satisfiable for n = 12. Then they use an LLM to help them write a Lean proof that the SAT solver input is equivalent to the human-readable description of what they wanted to prove.

I'm not disergarding the fact that LLMs don't generate text completely at random. They generate likely text. I suspect that can make it more likely to generate the text of some correct proofs. But I have no idea how likely that "more likely" is or what proofs are those.