The math is haunted
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 c