alt Hacker NewsIs that really a problem? The only risk in a Lean proof is the LLM finding a bug in multiple kernels (2 with the standard setup) that would let it add a new theorem without legitimately proving it. If you have reasoning traces or send a second model to look at the proof you can easily detect that and file a bug report.
For the rest you only need to check that the formal problem statement matches the actual problem and the proof is not using extra axioms. That's easy to check manually or with a simple script.
Many mathematicians care about understanding the method and the tools used more than the result. LLMs have a large advantage in memory and reading speed, you can feed them the entire internet and published literature at training time, and then make them check dozens of papers in a few minutes at runtime. They might not be very creative, but they've seen that obscure 1990's theorem in the training data that happened to use an idea that might just work again.
Reading the LLM's 12 MB lean output is a bit like trying to maintain a codebase that has been fully vibe-coded as a single giant file, by hand. Even if it's possible in principle, no one is going to enjoy that.