Lean Focused Research Organization - aVenture Non-Profit Research
Lean Focused Research Organization
Operating Status: Operating
Nonprofit advancing the Lean theorem prover and programming language for formal verification and mathematics.
The Lean Focused Research Organization (Lean FRO) is an independent nonprofit created to advance the Lean theorem prover and programming language, which is used for formal verification of software and mathematics. It funds and coordinates the core Lean development team, with support acknowledged from backers including Alex Gerko and Amazon.
Lean combines dependent type theory with an interactive proof development environment and is the basis of large formalization projects such as the Liquid Tensor Experiment and the formalization of Fermat's Last Theorem. The FRO stewards the language, its toolchain, and the Mathlib library ecosystem.
