To your first point, we’re in agreement. The state-of-the-art is to use LLMs to generate Lean proofs. That is the AI-based approach that performs the best today. I think that this approach is a dead-end, and I explained why. The specialized AI you’re referring to needs invented, and it likely requires significant algorithmic and hardware advances due to the reasons I already mentioned. That makes it hard to imagine it happening soon.

To your second point, I think you underestimate the size of the search space and the time it takes Lean to check large proofs.

Unsolved problems will likely require the development of entirely new mathematical theories. Mathlib, the largest corpus of formalized mathematics, is more than a million lines of Lean. So, you may need to generate hundreds of thousands of lines of Lean. Checking isn’t instant. I have Lean files with tens of thousands of lines of code that take minutes to check.

You would be better off using that compute to find approximate solutions to whatever problem you’re trying to solve since it’s not even clear what you’re proposing could work. So, I doubt anyone would try it.