July 30, 2025
For the past few months, I’ve been writing a lot of Lean.
Lean is a programming language, but it is mostly used by mathematicians. That is quite unusual! This is because Lean is designed to formalize mathematics.
Lean lets mathematicians treat mathematics as code—break it into structures, theorems and proofs, import each other’s theorems, and put them on GitHub.
The big idea is that eventually much of the humanity’s mathematical knowledge might be available as code—statically checked, verifiable, and composable.
So what does using Lean feel like?
To give you a taste of Lean, here is a tiny theorem that says 2 is equal to 2 :
theorem two_eq_two : 2 = 2 := by sorry
What’s going on here?
To a mathematician’s eye, this syntax looks like stating a theorem. We have the theorem keyword, the name or our theorem, a colon : before its statement, the statement that we’d like to prove, and := by followed by the proof ( sorry means that we haven’t completed the actual proof yet but we’re planning to fill it in later).
... continue reading