3 ms·
This is what Lean is for: https://lean-lang.org/ https://lean-lang.org/ If you have the LLM generate Lean code, and it compiles, then the proof is correct and
by jstanley 4mo ago
This is what Lean is for: https://lean-lang.org/ https://lean-lang.org/
If you have the LLM generate Lean code, and it compiles, then the proof is correct and you don't need to bother checking its working. (You still need to check that it is proving the theorem you asked it to prove).
- AaronAPU 4mo agoI’m playing devil’s advocate here, so go easy on me. But how completely do we know lean is perfectly true in all cases?
- bckgrndrdtn 4mo agoThere's a lot to be said about that: https://lean-lang.org/doc/reference/latest/ValidatingProofs/ https://lean-lang.org/doc/reference/latest/ValidatingProofs/ But let's assume Lean is perfect: - you have to trust your file system - you have to trust your OS - are you sure your monitor displays "proof is valid" correctly - maybe there's a bug in your CPU hardware? - or background radiation flipped a bit in your RAM - do you trust your brain? Maybe you went to bed last night firmly believing "that proof is wrong" and you woke up this morning with a different belief that "the proof is valid".
- pfdietz 4mo agoIf there's concern, I understand Lean can dump out a proof object, and this object can be checked for validity by a separate, smaller program. One could even write that smaller program multiple times. It would be interesting to see how Lean is being tested. Pummeling it with inputs from AI proof search engines sounds like a good way to expose hidden bugs, just as pummeling a compiler with randomly generated programs is a good way to expose previously unknown compiler bugs.