Lean FRO
The Lean Focused Research Organization, which develops Lean. Formed in July 2023 as a non-profit under Convergent Research, and described on its own About page as working "to make formal verification more accessible across mathematics research, software and hardware verification, and AI-assisted theorem proving," while "guiding Lean toward long-term self-sustainability."
Led by Chief Architect and co-founder Leonardo de Moura with Head of Engineering and co-founder Sebastian Ullrich. The FRO says many of its staff were recruited from the Lean community itself.
The funding, which is the unusual part
An open-source proof assistant with this many named backers is not the norm:
| Funder | Note |
|---|---|
| Alex Gerko (XTX Markets) | $10M in July 2025, split $5M to a new Mathlib Initiative and $5M to the FRO |
| Amazon Automated Reasoning | the largest single donation in the FRO's history, July 2026 |
| Alfred P. Sloan Foundation, Simons Foundation International, Richard Merkin Foundation | philanthropic |
| Convergent Research | the FRO's institutional host |
| Harmonic | inaugural donation February 2026; a startup built on Lean |
| BAIF (Beneficial AI Foundation) |
Two of those are worth separating from the rest. Harmonic sells a product built on Lean and funds the thing it depends on; Amazon uses Lean in production (Cedar, SampCert) and is also de Moura's employer. Neither is a conflict in any ordinary sense — an ecosystem paying for its own substrate is the healthy version of this — but it does mean the enthusiasm quoted on the site comes from parties with a stake in Lean succeeding, and the corpus should read the testimonials that way.
The "FRO" model itself
A Focused Research Organization is a fixed-term, mission-scoped non-profit designed to do work that neither academia nor a startup is shaped for — Convergent Research's model. The FRO's own language about "long-term self-sustainability" says the plan is to hand Lean off, not to run it forever. What that hand-off looks like is unstated, and it is the open question a wiki tracking this project should keep: a language with 9,007 GitHub stars and a national-lab-sized funding stack has no obvious steward after a time-boxed organization dissolves.
Related
lean-theorem-prover · leonardo-de-moura · mathlib · lean-lang-org · formal-verification