50 years of proof assistants
28 points by self
28 points by self
From the perspective of someone who has been idly interested in proof assistants from outside the field for the last decade or so, it's really remarkable how quickly Lean has seemingly taken over the pure mathematics niche (though not so much verifying real systems like CHERI or WebAssembly, as this essay discusses).
When I read about mathematicians like Terrance Tao doing machine-checked proofs, it's always with Lean. When I hear about some new proof being formalized, it's in Lean. University classes on formalization I come across like this one by Heather Macbeth are generally in Lean. All the LLM-assisted formalization startups I read about (Harmonic, Gauss, Axiom, maybe others I'm forgetting) are using Lean. DeepMind's 2024 silver IMO with AlphaProof was done in Lean.
Some of this is network effects I'm sure, but Lean is much younger than Rocq (formerly Coq) or Isabelle, so you'd think they'd have a head start. If anyone has a good history of why/how Lean "won" I'd love to read about it.
My guess is the effort put into mathlib. mathlib has become almost synonymous with Lean these days. No other proof assistant has such a centralised, singular entity of (math) proofs. Isabelle has the archive of formal proofs, but that's a bit more like a centralised repository of individual proofs, rather than one cohesive unit.
I think it was a lot easy for the (previously small) community to create such a centralised repository when it was small and new (from a social PoV) than for more established communities.
The nature of pure math means having a broad and "batteries-included" repository like mathlib is absolutely vital for formulating, let along proving, any non-trivial mathematical statements.
In addition to everything you said, it's also huge that Lean can be set up so easily. With elan (a literal fork of rustup), Lean has in some ways better tooling than most mainstream languages, and the VSCode extension can both automate first-time install and provide a fairly intuitive modern interface for interactive theorem proving.
Compare that to older proof assistants, which often expect you to manually install some crufty-looking language-specific IDE or to manually install and configure Emacs and a language-specific plugin and learn both the Emacs keybindings and language-specific plugin keybindings... I love (Cubical) Agda more than Lean, but it's not hard to see why stressed out grad students or less computer-savvy mathematicians have an easier time dipping their toes in the water with Lean.
This is specific to LCF, ML, and descendants. It's not about TLA+, Metamath, or other proof systems.