3 ms·

I do think that machine-verified proofs in strong systems like Lean are far superior to proofs merely verified by humans. Humans are amazing, but they also get

I do think that machine-verified proofs in strong systems like Lean are far superior to proofs merely verified by humans. Humans are amazing, but they also get bored and miss details. This isn't just a theoretical claim. People read Euclid's Elements for over two thousand years before noticing a missing axiom. That's the sort of basic mistake that any properly-working machine proof verification system would immediately reveal. Published math proofs are often later revealed to be wrong. The increasing sophistication of math means it's getting harder and harder for humans to properly verify every step. Machines are still not as good at creating proofs, but they're unequalled at checking them. There are "competing" systems to Lean, so I wouldn't say that Lean is the "one true way". I like Metamath, for example. But the "competition" between these systems needs to be in quotes, because each has different trade-offs, and many people like or use or commit to multiples of them. All of them can verify theorems to a rigor that is impractical for humans.

agalunar 2y ago
For the curious: I assume the parent is referring to Pasch's axiom. https://math.stackexchange.com/questions/1901133/euclids-elements-missing-axiom-of-m-pasch-examples https://math.stackexchange.com/questions/1901133/euclids-ele...
- dwheeler 2y ago
  Correct. The good news that Elements still works otherwise, you just need to add the missing axiom. But many other "proofs" have been found to be false. The book "Metamath: A Computer Language for Mathematical Proofs" (by Norm Megill and yours truly) is available at: https://us.metamath.org/downloads/metamath.pdf https://us.metamath.org/downloads/metamath.pdf - see section 1.2.2, "Trusting the Mathematician". We list just a few of the many examples of proofs that weren't. Sure, there can be bugs in programs, but there are ways to counter such bugs that give FAR more confidence than can be afforded to humans. Lean's approach is to have a small kernel, and then review the kernel. Metamath is even more serious; the Metamath approach is to have an extremely small language, and then re-implement it many times (so that a bug is unlikely to be reproduced in all implementations). The most popular Metamath database is "set.mm", which uses classical logical logic and ZFC. Every change is verified by 5 different verifiers in 5 different programming languages originally developed by 5 different people: * metamath.exe aka Cmetamath (the original C verifier by Norman Megill) * checkmm (a C++ verifier by Eric Schmidt) * smetamath-rs (smm3) (a Rust verifier by Stefan O'Rear) * mmj2 (a Java verifier by Mel L. O'Cat and Mario Carneiro) * mmverify.py (a Python verifier by Raph Levien) For more on these verifiers, see: https://github.com/metamath/set.mm/blob/develop/verifiers.md https://github.com/metamath/set.mm/blob/develop/verifiers.md
  - deleted 2y ago
    [deleted]

agalunar 2y ago

For the curious: I assume the parent is referring to Pasch's axiom. https://math.stackexchange.com/questions/1901133/euclids-elements-missing-axiom-of-m-pasch-examples https://math.stackexchange.com/questions/1901133/euclids-ele...

dwheeler 2y ago
Correct. The good news that Elements still works otherwise, you just need to add the missing axiom. But many other "proofs" have been found to be false. The book "Metamath: A Computer Language for Mathematical Proofs" (by Norm Megill and yours truly) is available at: https://us.metamath.org/downloads/metamath.pdf https://us.metamath.org/downloads/metamath.pdf - see section 1.2.2, "Trusting the Mathematician". We list just a few of the many examples of proofs that weren't. Sure, there can be bugs in programs, but there are ways to counter such bugs that give FAR more confidence than can be afforded to humans. Lean's approach is to have a small kernel, and then review the kernel. Metamath is even more serious; the Metamath approach is to have an extremely small language, and then re-implement it many times (so that a bug is unlikely to be reproduced in all implementations). The most popular Metamath database is "set.mm", which uses classical logical logic and ZFC. Every change is verified by 5 different verifiers in 5 different programming languages originally developed by 5 different people: * metamath.exe aka Cmetamath (the original C verifier by Norman Megill) * checkmm (a C++ verifier by Eric Schmidt) * smetamath-rs (smm3) (a Rust verifier by Stefan O'Rear) * mmj2 (a Java verifier by Mel L. O'Cat and Mario Carneiro) * mmverify.py (a Python verifier by Raph Levien) For more on these verifiers, see: https://github.com/metamath/set.mm/blob/develop/verifiers.md https://github.com/metamath/set.mm/blob/develop/verifiers.md
- deleted 2y ago
  [deleted]