Amazon is investing in the Lean Focused Research Organization
Captured source
source ↗Amazon is investing in the Lean Focused Research Organization - Amazon Science
Close
Close
Social
bluesky
threads
youtube
github
rss
Menu
Research
Research areas
Automated reasoning
Cloud and systems
Computer vision
Conversational AI
Economics
Information and knowledge management
Machine learning
Operations research and optimization
Quantum technologies
Robotics
Search and information retrieval
Security, privacy, and abuse prevention
Sustainability
Our scientific contributions
Publications
Research from our scientists and collaborators.
Conferences
Our experts present and discuss cutting-edge research at scientific meetings globally.
Research areas
Automated reasoning
Cloud and systems
Computer vision
Conversational AI
Economics
Information and knowledge management
Machine learning
Operations research and optimization
Quantum technologies
Robotics
Search and information retrieval
Security, privacy, and abuse prevention
Sustainability
Our scientific contributions
Publications
Research from our scientists and collaborators.
Conferences
Our experts present and discuss cutting-edge research at scientific meetings globally.
News & blog
The latest from Amazon researchers
Amazon Science Blog
Technical deep-dives and perspectives from our scientists.
News
Research milestones and recent achievements.
The latest from Amazon researchers
Amazon Science Blog
Technical deep-dives and perspectives from our scientists.
News
Research milestones and recent achievements.
Collaborations
Amazon Research Awards
Overview
Call for proposals
Latest news
Research stories
Recipients
Amazon Nova AI Challenge
Overview
Rules
FAQs
Teams
Research collaborations
Overview
Carnegie Mellon University
Columbia University
Hampton University
Howard University
IIT Bombay
Johns Hopkins University
Max Planck Society
MIT
Tennessee State University
University of California, Los Angeles
University of Illinois Urbana-Champaign
University of Southern California
University of Texas at Austin
Virginia Tech
University of Washington
Amazon Research Awards
Overview
Call for proposals
Latest news
Research stories
Recipients
Amazon Nova AI Challenge
Overview
Rules
FAQs
Teams
Research collaborations
Overview
Carnegie Mellon University
Columbia University
Hampton University
Howard University
IIT Bombay
Johns Hopkins University
Max Planck Society
MIT
Tennessee State University
University of California, Los Angeles
University of Illinois Urbana-Champaign
University of Southern California
University of Texas at Austin
Virginia Tech
University of Washington
Resources
Code and datasets
Amazon Nova
Try Amazon’s frontier foundation models.
Code and datasets
Amazon Nova
Try Amazon’s frontier foundation models.
Careers
Careers
Explore our open roles.
Amazon Scholars
Faculty research opportunities on industry-scale technical challenges.
Postdoctoral Science Program
Early-career research opportunities alongside experienced industry scientists.
Careers
Explore our open roles.
Amazon Scholars
Faculty research opportunities on industry-scale technical challenges.
Postdoctoral Science Program
Early-career research opportunities alongside experienced industry scientists.
Search
Submit Search
Automated reasoning
Amazon is investing in the Lean Focused Research Organization
As AI agents take on higher-stakes decisions, Lean programming language makes it possible to mathematically prove they will behave safely.
By Byron Cook , Shawn Bice
July 26, 2026
2 min read
Share
Share
Copy link
X
Line
QZone
Sina Weibo
分享到微信
x
Key takeaways
Amazon is providing long-term financial support to the Lean Focused Research Organization (FRO) to advance Lean, a programming language that enables mathematical proofs of software correctness. Amazon uses Lean-based verification across multiple products including Bedrock AgentCore for agentic safety, SampCert for differential-privacy guarantees, and AWS Neuron for AI chip compilation, with scientists using LLM-Lean combinations to prove complex distributed protocol correctness. Amazon supports Lean's development through the independent Lean FRO rather than internally to ensure transparency and trustworthiness, allowing customers, auditors, and regulators to independently validate proof tools for safety-critical AI applications.
Was this answer helpful?
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 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) — to make proof accessible to every developer in the world. This is the single largest donation in the FRO's history.
The Lean Focused Research Organization is building the tools that make mathematical proof practical at the scale of modern software.
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 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 uses...
Excerpt shown — open the source for the full document.