7 ms·
Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct? H
by skobes 13d ago
Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct?
How have we not merely substituted one verification problem for another?
- Legend2440 13d agoThe point of Lean is that it can be mechanically verified by a proof checker.
- sashank_1509 13d agoNot always, there can be bugs in lean. Recently some guy with claimed to disprove Collatz conjecture, only to turn out that there was a bug in lean. I actually have no idea, how anyone can be sure this 13 M lines is meaningful
- make3 12d agoLean is adversarial in a way. Lean is better thought of as a constraint language with a verifier that checks if the constraints are respected, than a programming language. Your job or the LLM's job is to write code that Lean is satisfied with, creating the link between what you're trying to prove, and mathematical axioms. If you write a bad proof, the Lean constraint checker will tell you, unless there are bugs in Lean itself, or you defined the goal constraint incorrectly.