Even beyond cheating with sorries or kernel bugs, the lean encoded theorems (or specifications) must be checked by humans to see if they truly mirror the real theorem authentically.

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, indeed correctly encode the real theorems. 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.

I just want to state that having "lean proofs" that build does not mean the actual real theorems we care about hold. Ultimately a human has to verify the lean encoded theorem statements 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.

Agreed that confirming “This proposition has been faithfully translated to Lean” matters. As a side note, though, this is an area where LLMs used interactively can be helpful.

Also in the case of these recent counterexamples turning up, we have good qualitative evidence that this pathway is effective.

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.

This is the Lean proof that a nonsofic group exists (34,440 lines): 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/94bc0feb6a9ff12c7d...

It 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.

In 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.