About

The Lean FRO

The Lean Focused Research Organization works 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 pursues 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 are 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