Amazon is investing in the Lean Focused Research Organization

Amazon is making the largest single donation in the history of the Lean Focused Research Organization (FRO) to support the development of Lean, a programming language that enables mathematical proofs of software correctness. The investment aims to make proof-based verification accessible to all developers, with applications in agentic safety, neurosymbolic AI, and critical infrastructure at Amazon, including Policy in Amazon Bedrock AgentCore and AWS Neuron. Amazon emphasizes that open, community-governed development of Lean is essential for transparency and trust in safety-critical AI.

We want to tell you about an investment we're making and why we're excited about it. As AI agents increasingly make decisions that move money, approve claims, and operate critical infrastructure, the standard approach to software testing is no longer sufficient. Testing checks the cases you thought of, but there is a fundamentally different approach: mathematical proof, which shows with certainty that a system cannot behave incorrectly, no matter what inputs it gets. Lean https://www.amazon.science/blog/how-the-lean-language-brings-math-to-coding-and-coding-to-math is a programming language with the potential to make correctness proofs practical at the scale of modern software. Amazon is now providing substantial, long-term financial support to the team building it — the Lean Focused Research Organization FRO http://lean-lang.org/fro — to make proof accessible https://www.amazon.science/blog/three-challenges-in-machine-based-reasoning to every developer in the world. This is the single largest donation in the FRO's history. Lean has spawned a thriving community of users in mathematics, computer science, physics, and many other fields. It has led to the creation of Mathlib, a comprehensive library of formalized mathematics, which ignited an explosion of further efforts in formalized proofs. And it has had a pivotal role in the development of AI reasoning capabilities: AI generation of formal proofs in Lean has been a key method for training models with lower error rates, to the point that they are now producing correct solutions to research-level problems. But to us at Amazon, the most exciting thing about Lean is the role it promises to play in agentic safety and neurosymbolic https://www.amazon.science/publications/a-neurosymbolic-approach-to-natural-language-formalization-and-verification AI: coupling generative AI with Lean's mathematical rigor will help enable verified, trustworthy AI agents. The Lean team drove this vision before the industry caught up, and it’s a vision that is increasingly important to our own strategy for agentic safety. For example, Policy in Amazon Bedrock AgentCore https://www.amazon.science/blog/demystifying-agents uses Lean-based verification to prove the correctness of the policy language that keeps AI agents within specified boundaries. We haven't seen anyone else offer this type of mathematical guarantee. Lean also underpins the correctness proofs behind systems such as SampCert mathematical guarantees that differential-privacy protections in AWS Clean Rooms are sound and AWS Neuron compilation to Amazon's AI acceleration chips . One scientist recently used an LLM with Lean to prove the correctness of Amazon Aurora's segment repair protocol, our most durability-critical distributed protocol, in a fraction of the time it would have taken manually. The set of applications is growing fast, and this is just the beginning. You might wonder why Amazon would want Lean developed in the FRO, outside of Amazon. The answer is that it's easier to trust a proof when you can evaluate the tools behind it yourself. Customers, auditors, and regulators can independently inspect and validate work done in community-governed tools, which is the kind of transparency that safety-critical AI demands. It also matters internally. Lean becomes more useful as its developer community which includes our engineers grows, providing more libraries, more tooling, and more formalized proofs for everyone. For both reasons, we have found it crucial that the foundational work on Lean happens in the open through the Lean Focused Research Organization http://lean-lang.org/fro .