5 ms·
This 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/
by nilkn 1mo ago
This 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 1mo 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 1mo 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.