alt Hacker NewsThe process of automating mathematics:
We understand the proof (most math from all of history) -> We understand how the proof was made (computer-assisted proofs like the four-color theorem) -> We have to trust the computer's explanation for how the proof was made (some LLM proofs)
Is 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.