> This one proof, the work of a hundred mathematicians or so, is tens of thousands of pages long and took half a century to complete. Now compare that to googl

> This one proof, the work of a hundred mathematicians or so, is tens of thousands of pages long and took half a century to complete. Now compare that to google3 or any other large software. It’s absolutely tiny. A paltry edifice in comparison both in pages and man hours as well as mathematical complexity. Boolean structures get monstrously huge. On the subject of proofs and the verbosity of traditional mathematical methods, this note[1] is interesting. It provides two fun little examples of shorter than normal proofs. It amuses me that just as mathematicians persisted in writing out “is equal to” for decades after Recorde gave us =, there will probably continue to be holdouts who write out “if and only if” instead of using ≡ for many years to come. [1] https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD1073.html https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD107...