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 migrate, the questions were always around how many bugs this system can find. What we soon realized is that actually finding bugs in code that was tested and in production for many years is not that valuable. Some of it is due to JavaScript being mainly used for UIs, so worst case scenario one often can just refresh the page (thankfully no one is writing mission critical software in JS, right?!?). And even more surprising the risk of fixing the “bug” that TS found was often higher, due to new errors that might arise.

If correctness wasn’t that big of a deal (especially over established codebases) what good is this type-checking? As I learned more about it, the following benefits emerged:

• TypeScript types power other tools - turns out whatever the correctness checker needs to connect say the definition of f and all call sites to verify that the arguments match the parameter signatures, is the same thing developer tooling needs to allow you to CTRL-click to definition, find all usages, refactor, etc.
• TypeScript types are a design language - once you get familiar enough one can use them as an initial language to spec design before the implementation. So a team of TS developers gets to share a mini-specification language for free, that they can use in early design before any runtime is even written.
• Immediate feedback correctness - TypeScript generally integrates with your IDE, so while checking correctness of already written and tested codebase is low value, having the correctness checks appear right underneath the code as you are writing it in the infamous “red squiggles” does offer big value, because of the immediacy. Caveats of course are, assuming one is not doing TDD and writing tests first, and the project is not too large when type-checking starts to bog down and can’t appear as you are typing.

Analogy with Lean and Math

So by analogy, formalizing math with Lean has the following similar benefits outside correctness and assistance in writing proofs.

• powering various math tools - instead of just writing LaTeX, and keeping all definitions in one’s head, with Lean one gets the very basic IDE support every programmer expects, but no informal mathematician gets - click-through definitions, hover over statements, auto-generated docs (like mathlib4_docs), non-string searching, refactoring, etc. For example, the Stacks Project is a very useful attempt to get some of these benefits without formalization, but formalization basically guarantees that every part of mathematics can generate something like this.
• analyzing meta-math trends - with fixed names of theorems and cross-project imports, one can generate more easily and reliably the meta-structures of mathematical proofs, which theorem uses which other ones. This enables automated discovery of alternative proof paths and visualization of the dependency graph of modern mathematics.
• repository and version control - if a result is retracted currently there is no guarantee that other results that depended on it would even know that happened and recursively retract their claims. Turning mathematical results into actual libraries with versions and dependency management will make the evolution of mathematical truth more streamlined.

Basically, the process of doing math will become more efficient and hopefully more pleasant. The price one has to pay is proving many more trivial proofs than they wish. Mathematicians are not against trivial proofs, textbooks are full of proofs that are “follow-your-nose” style. What is hard to accept, is that Lean will not allow anyone to control what they call “trivial”. To Lean everything needs a proof, but there are more and more powerful tactics being built, so “trivial” is what Lean’s current set of tactics can close in one-line, the rest need more work.

Finally, note that a lot of the benefits I am describing above don’t even need to have the full formal proofs, just formal statements are enough. This effort by Kevin Buzzard with support from Renaissance Philanthropy seems to confirm that just having statements is a very valuable task by itself - Renaissance Philanthropy formalized theorem statements.

Will these extra benefits tip the scale to make it worthwhile for mathematicians to change how they have been doing math for millennia, adopt new tools with steep learning curves? I hope so, but only time will tell.