About
The Lean FRO
The Lean Focused Research Organization is working to make formal verification more accessible across mathematics research, software and hardware verification, and AI-assisted theorem proving. Since its formation in July 2023 as a non-profit organization under Convergent Research, the FRO has pursued a focused 5-year mission to improve Lean's critical systems through enhanced scalability, usability, documentation, and proof automation while guiding Lean toward long-term self-sustainability.
The Lean FRO is led by Chief Architect and co-founder Leonardo de Moura, currently a senior principal applied scientist in the Automated Reasoning Group at Amazon Web Services. De Moura created Lean in 2013 and previously worked on automated reasoning and theorem proving at Microsoft Research and SRI International.
Working alongside de Moura is Head of Engineering and co-founder Sebastian Ullrich and a team of skilled researchers and engineers with specialized expertise across diverse aspects of Lean development. The Lean FRO team is globally diverse and many team members were recruited directly from the very active Lean community. The team actively engages with the community to promote Lean adoption across academic and industry contexts.
The Lean FRO gratefully acknowledges support from its funders and supporters, including Alex Gerko, Alfred P. Sloan Foundation, Richard Merkin Foundation, Simons Foundation International, and Convergent Research.
A Brief History of Lean
-
July 2025 - Lean awarded the 2025 Skolem Award for 2015 CADE paper "The Lean Theorem Prover (System Description)"
-
June 2025 - Lean awarded the 2025 ACM SIGPLAN Programming Languages Software Award
-
May 2025 - Over 50 university-level courses have been taught using Lean
-
February 2025 - Lean GitHub repository starred over 5,000 times
-
January 2025 - Mathlib4 GitHub repository exceeds 20,000 contributions
-
December 2024 - Over 30,000 installs of Lean 4 VS Code development environment in a single calendar year
-
September 2024 - Equational Theories project established
-
September 2024 - Lean Community Zulip channel grows to over 10,000 members
-
July 2024 - AlphaProof achieves IMO silver medal performance using Lean and Mathlib
-
June 2024 - Carleson project established
-
June 2024 - Harmonic launched, first startup based on Lean
-
April 2024 - Lean verification of AWS Cedar policies released
-
December 2023 - Fermat's Last Theorem project established
-
November 2023 - Polynomial Freiman-Ruza conjeture project established
-
September 2023 - Lean 4.0 official release
-
July 2023 - Mathlib ported from Lean 3 to Lean 4
-
July 2023 - Lean FRO founded by Leonardo de Moura and Sebastian Ullrich
-
June 2023 - LeanDojo presented at NeurIPS 2023
-
August 2022 - Aeneas verification toolchain presented at ICFP 2022
-
December 2021 - Liquid Tensor Experiment project completed
-
November 2021 - Lean Community Zulip channel grows to over 5,000 members
-
September 2021 - Lean GitHub repository starred over 1,000 times
-
August 2021 - Mathlib3 GitHub repository exceeds 10,000 contributions
-
May 2021 - Mathlib4 GitHub repository created
-
December 2020 - Liquid Tensor Experiment project established
-
October 2019 - Natural Number Game v1.0 released
-
January 2019 - The first Lean Together workshop hosted at Vrije Universiteit Amsterdam
-
April 2018 - Lean 4 development begins
-
February 2018 - Lean Community Zulip channel established
-
July 2017 - Mathlib3 mathematical library created
-
June 2017 - Big Proof Programme, focused on bringing proof technology into mainstream mathematical practice, at Isaac Newton Institute for Mathematical Sciences
-
January 2017 - Lean 3.0 official release
-
August 2015 - "The Lean Theorem Prover (System Description)" published at CADE-25
-
January 2015 - First university course taught using Lean, 15–815 Interactive Theorem Proving at Carnegie Mellon University
-
July 2013 - First commit to the Lean repository