>> LLMs are indeed very special compared to past efforts at automated theorem proving. The search tree for proofs is enormous, even short textbook exercises (i.e. a few dozen lines of Lean) were difficult with GOFAI techniques. Adding a few orders of magnitude to your compute budget barely moves the needle, since the search space increases exponentially for every line of the proof.

It depends what kind of automated theorem prover we're talking about. I'm not an expert on proof assistants like Lean. I am an expert on Resolution-based automated theorem provers and those can be implemented efficiently. For example, the SLD-Resolution based theorem prover used as the interpreter for Prolog (the logic programming language) runs in linear time and the cost of completing a proof is dominated by the cost not of the prover itself but the complexity of the theorem that is being proven. In more plain English when you run a Prolog program the cost that really matters is that of the program, not of the Prolog interpretation.

Now, I know that Resolution-based theorem provers aren't typically used in the same way as proof assistants let alone LLMs; but that is more of a historical accident than a limitation of the technique. There's no reason why one couldn't search for a proof of the Riemann hypothesis expressed as a Prolog program and using a Prolog engine. It's just not where most peoples' heads are these days.

>> Now LLMs have produced multi-thousand line Lean proofs. This is impossible by simply "try everything and see what sticks". LLMs are able to target their efforts to only promising proof strategies. Yes it helps that they work at superhuman speed, so they can try thousands of strategies where a human might try a dozen. But their results cannot be explained only by compute increases; they need genuine mathematical insight.

I understand the argument and I believe it has merit, but that's just to say that LLMs are trained to generate likely text, like I say in another comment. That is enough to explain the much improved ability to search quickly and efficiently (the LLM just has to generate text that looks like a proof; no need to actually carry out the steps of a proof) without recourse to 'genuine mathematical insight'. Which should be easy to believe because it's much harder to explain what 'genuine mathematical insight' is and where it comes from than it is to explain where the ability to predict likely text comes from: it's how LLMs are trained.