Comment by sheafification
13 hours ago
It’s highly nontrivial to verify that a 250k loc Lean program actually represents that which it claims.
I guess it could be AI turtles checking and summarizing all the way down, but is that any more credible than a single AI checking it? I doubt it.
> It’s highly nontrivial to verify that a 250k loc Lean program actually represents that which it claims.
Generally you only need to look at 10-100 lines (unless you have a highly novel theorem that essentially invents a new field of math or builds on a field that has never been worked on in Lean before) of the 250k to verify what it claims. This is why there is excitement around formal verification. The rest of it is perhaps useful to read to figure out why the proof works, but is not necessary for checking.
Human verification of the Lean program only requires verifying that the theorem itself is represented correctly. The theorem will only make up a very small part of the entire Lean program.