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 al

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.