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/EWD107...
https://en.wikipedia.org/wiki/Logical_biconditional has some nice comparisons of notation, including a mention that my old friend George Boole also used '='.
Take for example a single theorem: Classification of Finite Simple Groups [1]. 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.
Fermat’s Last Theorem [2] took 358 years to prove and required the development of vast amounts of theory that Fermat himself could scarcely have imagined.
[1] https://en.wikipedia.org/wiki/Classification_of_finite_simpl...
[2] https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem