Spotlight
What people are saying about Lean
"Lean has become a key enabler in scaling automated reasoning at Amazon. Its capacity to verify complex systems involving advanced mathematical concepts has transformed how we tackle problems once thought too complex or impractical. Lean is an indispensable tool in modern, large-scale software engineering, helping ensure soundness, correctness, and verified AI across our systems." — Byron Cook, Vice President and Distinguished Scientist, AWS
"Lean enables large-scale collaboration by allowing mathematicians to break down complex proofs into smaller, verifiable components. This formalization process ensures the correctness of proofs and facilitates contributions from a broader community. With Lean, we are beginning to see how AI can accelerate the formalization of mathematics, opening up new possibilities for research." — Terence Tao, Fields Medalist and Professor of Mathematics, UCLA
"At Google DeepMind, we used Lean to build AlphaProof, a new reinforcement-learning based system for formal math reasoning. Lean’s extensibility and verification capabilities were key in enabling the development of AlphaProof." — Pushmeet Kohli, Vice President, Research Google DeepMind
"Mathematical Superintelligence (MSI) with Lean will play a critical role in any industry where safety is paramount, including aerospace, automotive, and medical technology. In addition, we look forward to providing early access to our technology to students and researchers to accelerate advancement in mathematics, science, and engineering." — Tudor Achim, Co-Founder and CEO of Harmonic
"Lean is the core verification technology behind Cedar, the open-source authorization language that powers cloud services like Amazon Verified Permissions and AWS Verified Access. Our team rigorously formalizes and verifies core components of Cedar using Lean’s proof assistant, and we leverage Lean’s lightning-fast runtime to continuously test our production Rust code against the Lean formalization. Lean’s efficiency, extensive libraries, and vibrant community enable us to develop and maintain Cedar at scale, while ensuring the key correctness and security properties that our users depend on." — Emina Torlak, Senior Principal Applied Scientist, AWS
Featured News
Featured Projects
Amazon Science | Fermat’s Last Theorem | Mathematical Superintelligence (MSI)