Comment by sebzim4500
16 hours ago
It's nice to know that they didn't miss anything. The natural language proof is 10,000 pages and they have missed groups in the past.
16 hours ago
It's nice to know that they didn't miss anything. The natural language proof is 10,000 pages and they have missed groups in the past.
Indeed, this formalization effort spotted a flawed argument in one of the original publications and worked around it to repair the result.
How do we know the formalization itself doesn't have any errors? AFAIK it's very far from trivial to formalize something.
Well, the point of the _computer_ formalization is that it's checkable.
An error in the formalization would be a bug in lean. Which, as we know, certainly seems plausible (I've mused on if these giant proofs are incentivizing LLMs to find lean bugs to exploit), but at least it's a smaller surface area.
An error in the formalization could also be that you formally prove something different from what you think you proved.
In general checking that the definitions are correct isn't that hard and assuming at least one of the lean kernels you verify with is correct (which tbf is an assumption, the implementations are based on each other so could have a common bug) that's all you need to verify.
In this case the statement is unusually complicated but still much much easier to verify than the proof itself.
The papers describing lean and it's core operations are deliberately small. The kernel of a theorem prover is meant to be such that a human can check it for correctness. The kernel does not include things like type inference or execution. It literally checks the proof and that's all and everything needs to match exactly. It's fairly trivial to write such a thing.
Humans have to establish trust in this.
After that, the rest of the language is written. Yes it is possible the type inference engine is broken but in that case the kernel will reject it