The False Promise of Lean

"Mathematics is about ideas. Lean is about type-checking."

If you are a research mathematician, you have likely been accosted by the "formalization" evangelists. They promise a future where all mathematics is verified by computers, where bugs are impossible, and where AI helps you prove theorems.

They are lying to you.

What they are actually selling is a transformation of mathematics from a creative, insight-driven art form into a tedious software engineering task.

1. The Death of Intuition

In Lean, you do not manipulate mathematical objects; you manipulate syntax. The deep geometric or algebraic intuition that guides a proof is lost in a sea of tactics, type class resolutions, and implicit arguments. You stop thinking "why is this true?" and start thinking "how do I make the red squiggly line go away?"

You spend hours fighting the 'simplifier' because it decided to unfold a definition you wanted to keep abstract. You are not doing math; you are debugging a compiler error for a language that wasn't designed for humans.

2. The Unreadable Scroll

A mathematical proof is meant to be read. It communicates understanding from one human to another. A Lean file is a write-only cryptographic hash of a proof. It is unreadable. It explains nothing. It verifies, but it does not illuminate.

Have you ever tried to "read" a formalized proof in Mathlib? It is a sequence of incantations: simp, rw, apply. Without the interactive state of the editor, it is meaningless noise. We are building a library of Babel that no one can read.

3. The Versioning Treadmill

Mathematics is eternal. Euclidean geometry is as valid today as it was 2000 years ago. Lean code rots in months. The transition from Lean 3 to Lean 4 broke everything. Do you want your life's work to become a compile error next year?

They call it "progress." We call it planned obsolescence. If your proof depends on a specific version of a software library to be considered "true," is it really a mathematical truth?

4. The "AI" Delusion

"But AI will automate it!" This is the carrot on the stick. They want you to do the grunt work of formalizing libraries so they can train their models. You are not a mathematician to them; you are a data labeler.

Stop Wasting Your Time

Go back to your blackboard. Write proofs that humans can read. Leave the type-checking to the programmers.

Further Reading

• A Few Thoughts on the Lean Theorem Prover - An honest account of someone abandoning Lean after realizing the overhead.
• Why is formal proof so hard? (MathOverflow) - See the skeptical takes on the sheer effort required vs. the reward.
• SciLean - Even those trying to make it work for science admit it "jumps perhaps a bit rashly on the Lean train."