The point I'm most interested in is number 4: Arbitrary-Precision Verification. To my untrained eye it looks plausible.
Granted we are in the age of slop proofs and it is unfeasible to verify proof by hands, anyone can ask LLMs to create numerical tests of computable parts of a proof. And if it "blows-up" or behaves suspiciosly LLM will notice that.
This is a kind of software fuzzing, but for Lean proofs.
The problem is if you have no math cred (as is the case here, I presume), it's quite hard to get someone competent to read such disproval and verify its validity.
The point I'm most interested in is number 4: Arbitrary-Precision Verification. To my untrained eye it looks plausible.
Granted we are in the age of slop proofs and it is unfeasible to verify proof by hands, anyone can ask LLMs to create numerical tests of computable parts of a proof. And if it "blows-up" or behaves suspiciosly LLM will notice that.
This is a kind of software fuzzing, but for Lean proofs.
The problem is if you have no math cred (as is the case here, I presume), it's quite hard to get someone competent to read such disproval and verify its validity.
[flagged]