alt Hacker NewsI’m a little confused - I thought their proofs were all driven by Lean proofs - is that not right? So even if the quality of the work is low in some metrics, it either passes the test or not..? No space for changing your mind either way.
Replies
AlanYx • today at 8:57 AM
Only a subset contain Lean formalizations. And even for that subset, there's the potential that the formalization is semantically off (that is, it's a formalization for a slightly different problem).
stavros • today at 8:55 AM
If you wrote twenty million lines of Lean to verify something, my suspicion is you've been fuzzing the Lean solver rather than coming up with new math.
➕ show 1 reply
nialv7 • today at 10:05 AM
right now about 42% has Lean formalization I think.
No, in their original blog they wrote:
> As part of our GitHub repository, we are sharing formalizations of many of the proofs in Lean, a programming language that allows mathematical proofs to be checked by a computer. We will update the repository with more formalizations as we obtain them.
Meaning they published all results before checking all of them, and intended to add more Lean proofs later. In the linked post they state ~42% of the posted results now have formalized proofs, some were added, some verified, and I assume this means that some results turned out to be wrong.