4 ms·

Great read, I was expecting it to bring up the four color theorem, but it was actually an even more interesting debate touching on some modern mathematics. I t

• Animats 3y ago
  > In the 70's, this wasn't considered a 'real' proof. I ran into that decades ago. We used the original Boyer-Moore theorem prover [1] as part of a program verification system. The system had two provers, the Nelson-Oppen simplifier (the first SAT solver) to automatically handle the easy proofs, and the Boyer-Moore system for the hard ones. To make sure that both had consistent theories, I used the Boyer-Moore prover to prove the "axioms" of the Nelson-Oppen system, especially what are usually called McCarthy's axioms (the ones that use Select and Store) for arrays. The Boyer-Moore system uses a strictly constructive approach to mathematics. It starts from something like Peano arithmetic (there is a number zero, and an operation add 1) and builds up number theory. So I added a concept of arrays, represented as (index, value) tuples in sorted order, and was able to prove the usual "axioms" for arrays as theorems. The machine proofs were long and involved much case analysis.[2] I submitted a paper to JACM in the early 1980s and got back reviews saying that it was just too long and inelegant to be at the fundamentals of computer science. That might not be the case today. A few years back, I put the Boyer-Moore prover on Github, after getting it to work with Gnu Common LISP. So you can still run all this 1980s stuff. It's much faster today. It took about 45 minutes to grind through these proofs on a VAX 11/780 in the early 1980s. Now it takes about a second. The proof log [2] is amusing. It's building up number theory from a very low level, starting by proving that X + 0 = X. Each theorem proved can be used as a lemma by later theorems, so you guide the process by giving it problems to solve in the right order. By line 1900, it's proving that multiplication distributes over addition. Array theory, the new stuff, starts around line 2994. The reason this is so complicated and ugly is that there's no use of axiomatic set theory. Arrays are easy if you have sets. But there are no sets here. Sets don't fit well into this strict constructive theory, because EQUAL means identical. You can't create weaker definitions of equality which say that two sets are equal if they contain the same elements regardless of order, because that introduces a risk of unsoundness. Effort must be put into keeping the tuples of the array representation in ascending order by subscript, which implies much case analysis. Mathematicians hate case analysis. Computers are good at it. [1] https://github.com/John-Nagle/nqthm https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temporaryrulebaseprooflog.txt https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
• peteradio 3y ago
  If you have to rely on the computer to validate a proof you then have to rely on the whole supply chain that generated the computer as well as the software for the proof checker. Proofs need to be dense enough that we can discover them in a long lost tomb and eventually figure out what that collapsed civilization had learned.
  • ykonstant 3y ago
    > If you have to rely on the computer to validate a proof you then have to rely on the whole supply chain that generated the computer as well as the software for the proof checker. This is true, but a similar problem plagues typical proofs. > Proofs need to be dense enough that we can discover them in a long lost tomb and eventually figure out what that collapsed civilization had learned. This is almost never the case for modern mathematical research. Case in point, some of my current work relies on the classification of finite simple groups. Therefore, in practice, it is impossible to validate my results from first principles.
    • peteradio 3y ago
      Why does that classification preclude validation? Is that classification not imposed as part of your proof? I guess what I'm not so seriously wondering is what is the point of it, if it can't be understood without relying on a stupidly complex network?
  • c7b 3y ago
    Yes, but you only need one machine for all proofs (that its internal logic can represent), so all the efforts towards removing flaws from that system benefit all proofs, whereas classic review only ever benefits a particular proof (and other theorems that build on it). It just scales better. And that's probably what's needed to keep up with the pace of modern research. It's not unheard of for proofs to be citing theorems that were only published on arxiv. It's not even unheard of for proofs that were published in reputable journals to be retracted because errors were discovered later: https://retractionwatch.com/2022/11/18/mathematician-requests-two-retractions-for-subtle-inaccuracies/ https://retractionwatch.com/2022/11/18/mathematician-request... https://retractionwatch.com/2017/07/12/author-shocked-top-math-journal-retracts-paper/ https://retractionwatch.com/2017/07/12/author-shocked-top-ma... Prof. Byron Cook (pure math at UCL) is arguably a driving force behind a lot of the recent adoption of theorem provers. He's talked a lot about those problems (in fact, I was partially paraphrasing him from memory above). You can read up on what he said directly, I found it pretty convincing that proof verification is where modern mathematics should be moving towards (and probably will, there are collaborative efforts to re-prove substantial parts of modern mathematics using automated provers). Btw, do you have any support for your claim that proofs must be dense enough to fit onto a tombstone? I've literally never heard that before, and by your definition, pretty much no recent mathematical research would qualify. We've come a long way since Euclid.