Comment by returningfory2
2 hours ago
I feel this comment is based on a misunderstanding of how Lean works. In Lean you don't need to inspect the proof. There is no "closer inspection". All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
That's exactly what the navier stokes paper posted yesterday pointed out where the LLM bends the Lean code to make it "compile", because the NL might be wrong to begin with or because it missed a detail:
https://arxiv.org/html/2610.08144v1#S2
For complex / tedious proofs I can easily see how small details like this can lead to a valid lean proof (or valid "code"), but missing the important details that got lost.
That is an idealized caricature, and far from the reality. One needs to validate the statement of the theorem and the boundary conditions needed to prove it (definitions, axioms, kernel soundness, etc), a la dependency injection. Mathlib is a common shared platform of vetted truths, but not all proofs restrict themselves to Mathlib AFAIK, and neither is Mathlib perfect -- particularly subtle mismatches in the definitions.
Oh I fully understand how Lean works, how minimal the kernel is etc. I just think that just because "it compiled", we don't actually know that the autoformalization proved all the right stuff along the way. After all, LLMs can produce correct proofs for statements that don't align with the original intended theorem [1]. I just think we should be a bit more skeptical in general before saying these seminal results are fully true. What's the rush?
[1] - https://arxiv.org/abs/2610.08144
How much lean code do you need to read to check if NAvier-Stokes was correctly formalized?
A tiny fraction compared to the proof, I'm guessing.
But the point is that you don't need to check the proof. But a lot of people seem to misunderstand what's happening and think you still need to check the Lean proof that AI outputs.