About 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 the Lean programming language and proof assistant toward long-term self-sustainability.
Capability targets
Scalable Verification Systems
Infrastructure capable of handling million-line proofs and massive mathematical corpora, enabling research at the true frontier without technical bottlenecks.
Computable Mathematical Papers
A unified environment where mathematicians can interleave prose, familiar mathematical notation, and Lean code to produce both formally verified proofs and conventional-looking papers. This bridges informal exposition and machine-checkable rigor.
Trustless Knowledge Exchange
A new foundation for scientific collaboration where proofs, models, and computations can be shared, audited, and reused without dependence on personal reputation.
Universal Proof Verification
A shared infrastructure for machine-checkable mathematics, ensuring that any theorem or proof can be verified independently of human authority or institutional trust.
Leadership team
Supported by
Alex Gerko
Alfred P. Sloan Foundation
Richard Merkin Foundation
Simons Foundation International
