5 ms·

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

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.
- peteradio 3y ago
  Not onto a tombstone, in a tomb. Even the commandments required multiple tablets, two or three I suppose.
  - c7b 3y ago
    What's the size of a tomb? Is there some kind of symbol limit? Modern proofs easily run into the hundreds of pages, is that too long? And do you have any support for those requirements, or is that just your personal conviction?
    - peteradio 3y ago
      You are limited to 100 cubits cubes and must include all sources fully expanded on high quality papyrus scrolls. I have high quality sources for my personal convictions unfortunately I cannot provide them in this medium for they are on high quality papyrus.

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.

peteradio 3y ago
Not onto a tombstone, in a tomb. Even the commandments required multiple tablets, two or three I suppose.
- c7b 3y ago
  What's the size of a tomb? Is there some kind of symbol limit? Modern proofs easily run into the hundreds of pages, is that too long? And do you have any support for those requirements, or is that just your personal conviction?
  - peteradio 3y ago
    You are limited to 100 cubits cubes and must include all sources fully expanded on high quality papyrus scrolls. I have high quality sources for my personal convictions unfortunately I cannot provide them in this medium for they are on high quality papyrus.