Lean is making mathematicians apologize over and over
In Lean, skipping a step in a proof means typing one word, sorry. A short history of that word, and what it says about how much math is still left to formalize.
As a mathematician, this is one of my favorite things about the tool. Lean is a free, open-source programming language where you write math proofs and a computer checks every single step. It’s also how AI labs check that an AI’s proof is actually correct, not just confident.
But here’s the fun part.
When you can’t prove a step yet, Lean lets you skip it. You just have to type one word:
sorryAnd Lean replies: declaration uses 'sorry'
So picture it: brilliant mathematicians, engineers, PhDs, professors, typing sorry… sorry… sorry… dozens of times. Big projects have hundreds of them. A formalization is basically a list of apologies, and progress means taking them back one by one.
I went digging for who made this choice. It goes back to 1999: Markus Wenzel added sorry to the Isabelle proof assistant. It only worked in a mode literally called quick_and_dirty, and in the source code the function behind it was named cheat_meth.
Fifteen years later, in July 2014, Leonardo de Moura added sorry to Lean. The very next day he added a warning: “imported file uses sorry”. So your apology follows everyone who builds on your work.
And I think there’s something deep hiding in the joke.
In normal math (and normal life), sometimes we skip steps. Lean makes you apologize every time you do.
And there’s still a lot of apologizing left to do. Lean’s main math library has about 290,000 theorems, which sounds like a lot until you realize it barely reaches the edge of modern research. Some undergraduate topics are still missing. In my own field, complex algebraic geometry, most of the objects I worked with in my PhD can’t even be defined in Lean yet.
Whether we will actually get there, and how fast, is an interesting question in math right now. Especially because AI is now writing proofs too.