Post #4296010

"I have only made this letter longer because I have not had the time to make it shorter." (Blaise Pascal, often misattributed to Mark Twain) I have previously written about the evolving impedance mismatch between proof generation, proof verification, and proof digestion in mathematics. This has led to the following unintuitive breakdown of monotonicity, already noticed by Pascal as far back as 1657: it is now easier to generate long correct proofs than it is to generate short correct proofs! However, it is far more challenging to *verify* and *digest* such proofs, thus exacerbating the impedance mismatch. I have encountered this phenomenon personally with the Integrated Explicit Analytic Number Theory Network (IEANTN) project https://www.ipam.ucla.edu/news-research/special-projects/integrated-explicit-analytic-number-theory-network/ . As part of this project, a large number of lengthy technical papers in explicit analytic number theory are to be formalized. This was a tedious task, involving a lot of numerical verifications, and until recently was the bottleneck for the project; I could assign individual lemmas to formalize as tasks, and expect it to take weeks before a volunteer would claim them and prove them. Because the task of formalization by hand was difficult, the volunteer would naturally strive to make the proofs short, efficient, and natural, and as such they were easy to review by myself. (1/3)