lean-lang.org — the official site, and a four-year adoption chronology

Lean's own front page plus its FRO "About" page, read 2026-09-06 after arriving via Telegram. Two documents doing different jobs: the front page sells the tool, and /fro/about carries "A Brief History of Lean," a month-by-month chronology running from August 2022 to September 2026 with a link on nearly every entry.

Tier is split, deliberately. The front page is T1 for what Lean is — the feature inventory, the kernel design, the code samples, the governance and funding structure are the project describing itself and are checkable against the artifact. The timeline's impact entries and the four executive testimonials are T3: a self-curated selection of good news with no stated inclusion criteria, from the organization whose funding depends on the story. Both readings are useful. Neither should be quoted as an independent assessment.

What the site says Lean is

The one-line self-description leads with the language, not the prover: "Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code." Four capabilities are given headline treatment:

• grind — the automation tactic shipped in Lean 4.22.0 (August 2025). The front-page samples use it to discharge pattern matching and case analysis "beyond standard tactics," and to solve systems of linear integer inequalities outright. The longer sample proves the infinitude of primes with grind doing most of the work.
• A minimal trusted kernel — "guarantees absolute correctness in mathematical proof, software and hardware verification." The claim the whole certificate argument in lean-certificate rests on.
• Extensible metaprogramming — users add domain-specific notation and new proof automation. The prime-number sample defines n ! as custom notation in two lines.
• Mathlib — "over a million lines of formalized mathematics spanning algebra, analysis, topology, probability, and computer science."

Governance and money are stated on the page rather than hidden: development runs through the Lean FRO, funded by Alex Gerko (XTX Markets) plus the Alfred P. Sloan Foundation, Convergent Research, the Richard Merkin Foundation, Simons Foundation International, Harmonic, BAIF and Amazon Automated Reasoning. Not stated anywhere on the front page: the licence. The GitHub API gives it as Apache-2.0 for both leanprover/lean4 and leanprover-community/mathlib4.

Verification is leaving mathematics, on the site's own showing

The "Lean in Action" strip is the part that has changed most since this wiki first paged Lean in May. Five of its six featured projects are not mathematics:

Emina Torlak (AWS) describes the Cedar workflow in a detail worth keeping, because it is not the usual proof-assistant story: the team formalizes Cedar in Lean and then "leverages Lean's lightning-fast runtime to continuously test our production Rust code against the Lean formalization." Lean is being used as an executable oracle in CI, not only as a place to write proofs. That is the "programming language" half of the tagline doing real work, and it is why the site leads with it.

Byron Cook (AWS) makes the wider claim on the same page: Lean "has become a key enabler in scaling automated reasoning at Amazon." Amazon Automated Reasoning made the largest single donation in the FRO's history in July 2026. Read the endorsement with the donation next to it.

The chronology as a first-party adoption curve

The FRO history is the most complete adoption record this wiki holds for any single technology, and it lands squarely in cluster F's open problem. Its own numbers:

Also on the record: the Zulip community passed 10,000 members in September 2024, Lean won the 2025 ACM SIGPLAN Programming Languages Software Award and the 2025 Skolem Award, and the funding line runs $10M from Alex Gerko in July 2025 (half of it to a new Mathlib Initiative) through Harmonic's inaugural donation in February 2026 to Amazon's record gift in July 2026.

Every one of those is a numerator. adoption-curve-measurement found that cluster F's four shape-models cannot place a technology on its own curve while it is happening, and that the deepest reason is the absence of a denominator; org-mode-adoption hit the same wall from the other direction. Lean is a third instance and the cleanest one yet, because here the vendor itself is publishing the series and still cannot say what fraction of anything it represents. Nobody knows how many people would use a proof assistant if they knew about it, so 9,007 stars and 100,000 installs locate Lean precisely inside formal methods and not at all on an S-curve.

The list also reproduces the cluster's other standing complaint — a number that looks longitudinal and is not. "Over 30,000 installs in a single calendar year" (2024-12) and "installed over 100,000 times" (2025-09) are an annual rate and a cumulative total, printed nine months apart in one chronological list where the natural reading is 3.3× growth. The corpus met exactly this shape in org-mode-adoption with the ~80-response 2007 poll beside the 7,344-response 2020 survey. It is not dishonesty; it is what happens when a promotional timeline is assembled from whatever number was available that month.

What the timeline does measure well

Composition, not size. Read as a sequence of kinds of entry rather than magnitudes, the history is unusually legible:

• 2022–2023: infrastructure. Aeneas, Iris-Lean, the Mathlib 3→4 port, Lean 4.0, the FRO itself.
• 2024: mathematics and press. PFR, Carleson, the Equational Theories project, AlphaProof's IMO silver, and the first non-specialist coverage (NYT, Nature, Scientific American).
• 2025: institutions and money. ACM and Skolem awards, the $10M Gerko grant, 50+ courses, the Mathlib Initiative, grind and a new compiler, plus the first startups (Harmonic, Axiom).
• 2026: AI systems and industry. Aristotle, AlphaProof Nexus, Leanstral, Pramaana Labs' $27M seed, Comparator, Lean Eval, Palomar, Tau Ceti, StatLib, CSLib, Hex — and the frontier labs arriving in force with ten-proofs, the Riemann zeta formalizations, and Fermat's Last Theorem.

The pattern that emerges is a validation layer forming around AI output, which is the thesis lean-certificate states from the other side. Google DeepMind's July 2026 piece is named on the timeline as being about "AI conjecture machines and Lean as the validation layer for AI-generated science." Three months of 2026 entries are infrastructure for checking machines: Comparator (a sandboxed judge that re-checks independently), Lean Eval (a submission leaderboard of hard formalization problems), Palomar (a registry of Lean-verified mathematics), the Lean Kernel Arena (benchmarking independent proof checkers). None of those existed before AI started producing proofs at volume.

What is not here

No licence on the front page, no version number, no benchmark of Lean against Rocq or Isabelle, no count of active users as distinct from stars and installs, and no entry recording anything that went wrong. A four-year chronology with no failures in it is a marketing document about a real project, which is the correct way to read it.

Related

lean-theorem-prover · lean-fro · leonardo-de-moura · mathlib · lean-certificate · formal-verification · flt-formalization-anthropic · ten-proofs · autoformalization · adoption-curve-measurement · org-mode-adoption · technology-adoption-curve