3 ms·
It seems that a lot of folks misunderstand the guarantees that lean provides. I just want to state that having "lean proofs" that build (checks) does not mean
by rencrisa 2mo ago
It seems that a lot of folks misunderstand the guarantees that lean provides.
I just want to state that having "lean proofs" that build (checks) does not mean the actual real theorems we care about hold. Ignoring lean kernel bugs, ultimately a human (not an agent) has to verify the lean encoded theorem statements (specs/specifications) that the lean proofs are checked against. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal. AI generated lean encoded theorems can be huge and difficult to understand. I wonder if anyone reputable has audited these specifications.
- deleted 2mo ago[deleted]
- nilkn 2mo agoThis is the Lean proof that a nonsofic group exists (34,440 lines): https://github.com/openai/ten-proofs/blob/main/NonSoficGroup.lean https://github.com/openai/ten-proofs/blob/main/NonSoficGroup... This is an extraction from that of the actual theorem statement (39 lines): https://github.com/openai/ten-proofs/blob/94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6/ComparatorChallenges/D_NonSoficGroup.lean https://github.com/openai/ten-proofs/blob/94bc0feb6a9ff12c7d...
- rencrisa 2mo agoIt may be for this theorem there's a succinct description, but still needs to be checked carefully. However, there are others that are non-trivial.
- nilkn 2mo agoIn some cases you're right, but I think that's often a symptom of mathematics in Lean being relatively immature (i.e., it will get much easier with time). Even then, verifying the statement in Lean is correct is still much easier than verifying the natural language proof is correct.