July 30, 2026
Proof wars: the sequel
Are We Stuck with Lean?
Math nerds ask if Lean already won — and the comments turn into a tool war
TLDR: A mathematician asked whether Lean, the fast-rising tool for computer-checked proofs, has already become impossible to dislodge. The comments instantly split between tiny-kernel Metamath fans, skeptics nitpicking the comparison, and exhausted users saying this is just another classic nerd holy war.
A spicy question on MathOverflow basically asked the thing plenty of mathematicians have been whispering: has Lean become so dominant that everyone else missed their chance? Lean is a proof-checking tool for writing math in a computer, and the post wonders whether any serious group could still rally behind a rival like Metamath — or whether the train has already left the station.
But the real action is in the comments, where the vibes swing from earnest lobbying to full-on editor-war energy. One camp jumps in waving Metamath flags, bragging that its trusted checker is tiny — just a few hundred lines — which in this world is basically the equivalent of saying, "our engine is so simple you can inspect it with a flashlight." Another commenter pushes back hard, saying the whole "Lean is based on this, Metamath is based on that" framing is muddled anyway. Translation for non-specialists: even the people in the room can’t agree on what counts as a meaningful difference.
Then came the social drama. A Metamath contributor politely did the "every tool has pros and cons" routine, while another commenter dropped a cryptic bomb about a link in the replies sounding "pretty damning." And the funniest shot? One user compared the whole thing to Emacs users trying to force Vim users to switch — a gloriously old-school nerd feud that says everything. The strongest mood here is not just "which tool is best?" but "why are people trying to crown one king at all?"
Key Points
- •The MathOverflow post asks whether the mathematical community is now effectively committed to Lean as its proof assistant.
- •The author says that three years earlier there was still a possible window for mathematicians to rally around a proof assistant of their choice.
- •Lean’s earlier momentum is attributed to Kevin Buzzard’s Xena Project and Peter Scholze’s Liquid Tensor Experiment.
- •The post notes that Terry Tao had not yet learned Lean and that Mathlib’s migration from version 3 to version 4 had only just been completed at that time.
- •The author asks whether any organization could seriously support an alternative to Lean and suggests Metamath as a candidate.