Why formalize mathematics – more than catching errors

Summary

Why formalize mathematics - more than catching errors I read a good post by one of the authors of the Isabelle theorem prover, that got me thinking. The author, Lawrence Paulson, observed that most math proofs are trivial, but writing them (preferably with a proof assistant) is a worthwhile activity, for reasons similar to safety checklists - “Not every obvious statement is true.” As I have been a bit obsessed with doing formalized mathematics, this got me thinking about why I am excited to spend many hours recently writing formalized proofs in Lean for exercises from Tao’s Real Analysis (along with this recent attempt to write a companion to Riehl’s Category Theory In Context). On a very personal level, I just like math, computers and puzzles, and writing Lean proofs feels like doing all three at once. But I do believe formalization is important beyond nerd-snipping folks like me. While Paulson focuses on the obvious benefit of finding potential errors in proofs as they are checked by a computer, I will discuss some other less obvious benefits of shifting to formal math or “doing math with computers” as I tell my friends who ask me what I am obsessing over. To understand these benefits let me begin by sharing a parallel from my engineering career. TypeScript story TypeScript is an optional static type system for JavaScript (a dynamic language without static types). Very briefly, when writing TypeScript, one is roughly writing JavaScript with some extra annotations - types. Those are checked by the TypeScript compiler, as part of the compilation / build process. If the type annotations are not consistent - say you said the function f expects a number but somewhere you also wrote f('foo') an error will be emitted. If no such errors are found, the type annotations are erased and JavaScript is emitted for further execution. It seems all TypeScript is good for is catching errors and rejecting your programs. So when we went around Google pitching different teams to migra...