3 ms·
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
by sheafification 1mo 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.
- idiliv 1mo agoHuman 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.
- dwohnitmok 1mo ago> 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.
- deleted 1mo ago[deleted]