The Lean Theorem Prover: Design, Evolution, and Impact
We have never been more relevant
Formal verification makes AI trustworthy.
AI makes formal verification cost-effective.
Hex: Verified Computational Algebra
Hex is a Lean library for computational algebra: LLL lattice reduction, Gram–Schmidt, matrix row reduction, polynomial factorization.
Every algorithm is proved correct in Lean.
Specifications written by hand. Implementations and proofs written by AI.
Kim's blogpost demonstrates how to use Hex to perform Coppersmith's attack on RSA, recovering a 400-bit secret from a 2048-bit modulus.
Kim Morrison, July 2026.
Lean is a "Game"
"You have written my favorite computer game" — Kevin Buzzard, Prof. of Mathematics, Imperial College
def odd (n : Nat) : Prop := ∃ k, n = 2 * k + 1
theorem square_of_odd_is_odd : odd n → odd (n * n) := by
intro ⟨k₁, e₁⟩
simp [e₁, odd]
exists 2 * k₁ * k₁ + 2 * k₁
lia
The "game board": you see goals and hypotheses, then apply "moves" (tactics).
Each tactic transforms the game board.
The kernel checks the final proof term.
Lean: The First 10 Years
Lean 3: The Prover Becomes Programmable
Released January 2017, with a tutorial at POPL 2017.
First Lean version with a real tactic framework.
Tactics are written in Lean itself.
"A Metaprogramming Framework for Formal Verification" — ICFP 2017.
This design made community automation possible: linarith, ring, omega, and hundreds more.
The community implemented several linters in Lean.
Lean: The First 10 Years
Mathlib: The Lean Mathematical Library
Created in July 2017, in Lean 3 during Big Proof. An open-source, community-driven library. Today:
-
280,000+ formalized theorems.
-
2.4M+ lines of Lean. 50,000+ lines of extensions.
-
750+ contributors.
-
1,500+ type classes, 20,000+ instances.
"I'm investing time now so that somebody in the future can have that amazing experience." — Heather Macbeth, Prof. of Mathematics, Imperial College
Lean: The First 10 Years
Lean 4: Implemented in Lean
Sebastian Ullrich and I started development from scratch in April 2018. At the time, Mathlib was just ~55K LoC.
Goal: Implement compiler, elaborator, parser, tactic framework, and build system in Lean.
-
October 2020: Lean 4 compiles Lean 4.
-
January 2021: First pre-release. Mathlib is ~450K LoC.
-
September 2023: Lean 4.0 official release with Mathlib fully ported (~1.1M LoC).
-
Lean 4 is very extensible.
Lean: The First 10 Years
The Liquid Tensor Experiment
November 2020: Peter Scholze posed a formalization challenge.
"I spent much of 2019 obsessed with the proof of this theorem, almost getting crazy over it. I still have some small lingering doubts." — Peter Scholze
Johan Commelin led a team that verified the proof, with only minor corrections.
They verified and simplified the proof without fully understanding it.
"The Lean Proof Assistant was really that: an assistant in navigating through the thick jungle that this proof is." — Peter Scholze
Lean: The First 10 Years
The Lean FRO
Nonprofit. 20 engineers. Open source. Controlled by no single company.
Sebastian Ullrich and I launched it in July 2023.
Lean is not a research project anymore. We run the Lean FRO as a startup.
32 releases and 9,000+ pull requests merged since launch.
Mission focus: scalability, usability, proof automation, documentation.
The Lean project was featured in NY Times, Quanta, Scientific American, Wired, and others.
What is Lean Today?
A programming language and a proof assistant.
Lean is implemented in Lean. Very extensible.
Lean is scalable.
Small trusted kernel. Proofs can be exported and independently checked.
285,000+ unique installations: VS Code (161K) + Open VSX (126K).
def reverse : List α → List α
| [] => []
| x :: xs => reverse xs ++ [x]
theorem reverse_append (xs ys : List α)
: reverse (xs ++ ys) = reverse ys ++ reverse xs := by
induction xs with
| nil => simp [reverse]
| cons x xs ih => simp [reverse, ih]
#eval reverse [1, 2, 3]
Mathlib Growth and Build Cost
Instructions to build Mathlib, measured for every commit by radar, our performance-tracking server.
Compared with January 2025: 44% more code, 10% fewer instructions to build.
Green: Lean releases. The sharp drops correspond to compiler and automation improvements.
Mathematics Is Adopting Lean
Six Fields Medalists engaged: Tao, Scholze, Viazovska, Gowers, Hairer, Freedman.
-
Carleson's Theorem (completed) — van Doorn
-
Liquid Tensor Experiment (completed) — Commelin
-
The Polynomial Freiman-Ruzsa Conjecture, Tao (completed)
-
Equational Theories Project, Tao (completed)
-
Sphere Packing — Birkbeck, Hariharan, Lee, Ma, Mehta, Viazovska
-
Fermat's Last Theorem — Buzzard
-
Inter-Universal Teichmüller Theory — Mochizuki
At this scale, mathematics needs build systems, dependency graphs, code review, release engineering, and a precise medium for communication.
Reading vs Writing Formal Math
-
It is easier to read formal math than write it.
-
Formal math is easier to read than LaTeX.
-
You can click through, inspect definitions, check types.
-
AI can explain formal proofs and is making the writing part easier.
Verso: Type-Checked Documents
-
Future math papers will embed type-checked Lean code.
-
Lecture notes, papers, and slides in one tool.
-
These slides are written in Verso.
-
Every example is checked by Lean.
-
lean-lang.org is written in Verso.
-
My homepage is written in Verso.
-
Verso is a domain-specific language embedded in Lean.
-
Built by David Thrane Christiansen at the Lean FRO.
Verso Blueprint: A Map for Large Formalizations
-
Verso Blueprint is the next generation of Massot's Lean Blueprints, which are widely adopted in the Lean community.
-
Large projects like FLT and Sphere Packing need more than proofs.
-
It tracks definitions, lemmas, and dependencies.
-
The blueprint is a Lean document with inline code that is type-checked.
-
Built by Emilio Jesús Gallego Arias at the Lean FRO.
-
Emilio ported major projects onto it: FLT, Carleson, Sphere Packing.
Lean Verbose
Lean Verbose provides natural-language tactics to teach mathematics using Lean 4.
Playing the Lean game using mouse clicks and natural language.
Lean Verbose is implemented in Lean by Patrick Massot.
Lean Workbench (Coming Soon)
-
Zero installation. Manage Lean and Verso Blueprint projects in your web browser.
-
Pre-configured with AI.
-
Great for teaching. Students can focus on the course instead of the technology.
-
Instructors can ensure students use the correct libraries for the course.
-
Built by Jason Reed at the Lean FRO.
What We Learned from Mathematics
-
Machine-checkable proofs enable a new level of collaboration.
-
It is not just about proving but also understanding complex objects and proofs, getting new insights, and navigating through structures beyond our cognitive abilities.
-
Formal math is more maintainable: auto-refactoring and generalization for free.
"We had formalized the proof with this constant 12, and then when this new paper came out, we said, 'Okay, let's update the 12 to 11.' And what you can do with Lean is that you just in your headline theorem change a 12 to 11. You run the compiler and... of the thousands of lines of code you have, 90% of them still work." — Terence Tao, Lex Fridman interview
AI now writes the proofs
Lean checks them.
"Vibe Proving"
Alexeev & Mixon resolved a $1000 Erdős prize problem.
"We used ChatGPT to vibe code a Lean proof." — Alexeev & Mixon
The proof is machine-checked. Paper
International Mathematical Olympiad (IMO)
Every medal-level IMO AI with formal proofs uses Lean.
-
AlphaProof (Google DeepMind) — silver medal, IMO 2024
-
Aristotle (Harmonic) — gold medal, IMO 2025
-
Seed Prover (ByteDance) — silver medal, IMO 2025
AI plays the Lean game.
The moves in this game are tactics from automated reasoning.
Some moves played by AlphaProof:
simp_all [Finset.sum_range_id]
zify [*] at *
norm_num at *
nlinarith [(by norm_cast : (c:ℝ) ≥ A*(l-⌊_⌋)+⌊_⌋+1),
Int.floor_lex, Int.lt_floor_add_one x]
Even the most advanced AI relies on the same tactics we use every day.
Better tactics make more powerful AI.
AI Startups
-
Leanstral (Mistral): the first open-source code agent designed for Lean 4.
-
Axiom: solved 12/12 problems on Putnam 2025.
-
DeepSeek Prover-V2: 88.9% on miniF2F. Open-source, 671B parameters.
-
Harmonic: built the Aristotle AI — gold medal, IMO 2025.
Sphere Packing
Sidharth Hariharan and collaborators describe how Viazovska's Fields Medal-winning sphere packing proofs were formally verified in Lean.
"They Spent Years on a Math Problem. Then They Were Scooped by A.I." — NY Times
"We've gotten Gaussed." — Maryna Viazovska
The effort culminated in the autoformalization of the 24-dimensional sphere packing proof, over 200,000 lines of code, in just two weeks.
zlib in Lean
AI converted zlib (a C compression library) to Lean.
theorem zlib_decompressSingle_compress (data : ByteArray) (level : UInt8)
(maxOutputSize : Nat) (hsize : data.size ≤ maxOutputSize) :
ZlibDecode.decompressSingle (ZlibEncode.compress data level) maxOutputSize = .ok data
"The Lean library isn't just tested and validated, it's proved correct. This allows us to let AIs loose optimizing the code, requiring that they update the proof whenever the implementation materially changes. This gives us the confidence to allow them to work autonomously in a way that would be unthinkable in other languages." — Kim Morrison, Why Lean is faster than Rust
Radix: 10 AI Agents, One Weekend
10 AI agents built a verified embedded DSL with proved optimizations in a single weekend.
-
52 theorems.
-
5 verified compiler optimizations.
-
Determinism, type safety, memory safety.
-
Interpreter correctness — sound and complete.
-
27 modules, ~7,400 lines of Lean.
-
I did not touch the code. Zero lines. Full agent autonomy.
Formal Frontiers
A Mathlib Initiative project.
Defines community standards for trustworthy, maintainable autoformalization.
Releases open-source tooling for scalable AI-driven formalization workflows.
Produces high-quality Lean artifacts that fill important gaps in Mathlib.
Provides prerequisites for research-level formalization.
Tau Ceti: AI-Authored Lean Mathematics
-
AI-authored Lean mathematics, directed by a human-owned roadmap and gated by open, adversarial review.
-
Humans own the roadmap: mathematicians choose the targets.
-
AIs write and review the code.
-
On the roadmap: universal covers, the Jacobian challenge, reductive algebraic groups, PDEs.
To turn any computer into a Tau Ceti contributor:
uv tool install git+https://github.com/kim-em/TauCetiWorker tauceti work --loop
AI Changed How I Work
AI is not just changing who uses Lean. It changed how I work.
Kim Morrison (Lean FRO) showed me a major refactoring step: more than 10,000 lines changed across Mathlib, implemented by AI.
Since then, AI has removed the pain of developing software.
I used to believe my superpower was that I could tolerate a lot of pain. That superpower is no longer relevant.
AI now isolates issues, tries new ideas, runs experiments, analyzes performance, and much more.
Lean Eval
-
Public results on a benchmark of hard Lean formalization problems.
-
Submission-based leaderboard.
-
Erdős's unit-distance conjecture is one of the problems.
-
OpenAI showed this 80-year-old conjecture to be false.
-
Boris Alexeev submitted a ~1.2M-line Lean formal proof.
-
"Human mathematicians are being outcounterexampled" — Kevin Buzzard
-
-
Feit–Thompson odd-order theorem — 4 submissions
-
Jacobian of a compact Riemann surface (Buzzard challenge) — 4 submissions
The Statement / Specification Is Your Responsibility
Formal Conjectures (Google DeepMind): curated, human-verified formal statements of open problems.
Validating Lean Proofs
"It's really important with these formal proof assistants that there are no backdoors or exploits you can use to somehow get your certified proof without actually proving it, because reinforcement learning is just so good at finding these backdoors." — Terence Tao
Lean has multiple independent kernels. You can build your own and submit it to arena.lean-lang.org.
Validating a Lean Proof ∣ Who Watches the Provers?
Lean Kernel Arena
arena.lean-lang.org benchmarks independent proof checkers on the same proofs.
Comparator
Comparator is a judge for Lean proofs. comparator.live.lean-lang.org
Avoids metaprogramming / unsafe exploits. Exports proofs. Sandboxed.
A challenge is a Lean file with sorrys to be filled.
def large : Nat := sorry
theorem large_lt : 37 < large := sorry
A solution replaces the sorrys with Lean terms and proofs.
def large : Nat := 38
theorem large_lt : 37 < large := by decide
Comparator checks whether the solution is valid.
Comparator in Action
A challenge asks for a proof of False.
A candidate tries to smuggle one past the kernel with a metaprogramming trick that exploits a missing check in the official kernel.
Real GitHub issue. Comparator rejects it. The proof is exported and re-checked independently, defeating the exploit.
Nanoda (Lean kernel written in Rust) and Lean4Lean reject it too.
Do We Still Need Proof Automation?
"I thought AI would prove all theorems for us now."
-
Tactics are like game moves.
-
Better tactics = shorter proofs.
-
Better tactics = more powerful AI.
-
Compact proofs = better training data = better AI provers.
What Is grind?
New proof automation, shipped in Lean v4.22. Kim Morrison and me.
A virtual whiteboard, inspired by modern SMT solvers.
-
Writes facts on the board. Merges equivalent terms.
-
Cooperating engines: congruence closure, E-matching, constraint propagation, guided case analysis.
-
Satellite theory solvers: cutsat (linear integer arithmetic), commutative rings (Gröbner), linarith, AC.
-
Native to dependent type theory. No translation to FOL.
-
Produces ordinary Lean proof terms. Kernel-checkable.
-
Talk at IJCAR (Monday July 27 at 11:50 am).
-
5,000+
grinduses in Mathlib.
grind — Theory Combination
example [CommRing α] [NoNatZeroDivisors α]
(a b c : α) (f : α → Nat)
: a + b + c = 3 →
a^2 + b^2 + c^2 = 5 →
a^3 + b^3 + c^3 = 7 →
f (a^4 + b^4) + f (9 - c^4) ≠ 1 := by
grind
Three solvers meet at the E-graph:
-
Ring solver derives
a^4 + b^4 = 9 - c^4. -
Congruence closure lifts it to
f (a^4 + b^4) = f (9 - c^4). -
Linear integer arithmetic closes
2 * f (9 - c^4) ≠ 1.
The Nelson-Oppen playbook. Inside dependent type theory. No SMT translation layer.
Better Tactics = Better AI
example {α} [CommRing α] [IsCharP α 0] [NoNatZeroDivisors α]
(d t d_inv : α)
(Δ40 : d * (d + t + d * t) = 0)
(Δ41 : d^2 * (d + d * t - 2 * d * t^2 + d * t^4 + d^2 * t^4) = 0)
: d * d_inv = 1 →
t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by
grind
Quantum algebra example from "Categories generated by a trivalent vertex" — Morrison, Peters, Snyder.
When grind closes a goal in one step instead of fifty, the AI search tree shrinks dramatically.
What We Learned from AI
Autoformalization is already effective.
AI is getting better and better at explaining Lean code.
AI can already synthesize code from specifications.
Software Foundations in Lean: translated by humans. The AI translation is good, but making it great takes more effort than writing from scratch.
In 2019, the IMO was posed as a Grand Challenge for AI. Five years later, it feels routine.
AI is exceptional at the nerd-sniping tasks: isolating and diagnosing bugs, optimizing code, translating code, writing complex proofs, and metaprogramming.
But it is not good at system-level engineering and design, novel implementation and design ideas, or long-running contexts.
Software Verification
Lean is not only for mathematics.
Cedar (AWS): Verified Authorization
Cedar — open-source authorization policy language. Used by AWS Verified Permissions and AWS Verified Access.
Cedar spec: the model is written in Lean.
Three examples of verified components: evaluator, authorizer, validator.
-
forbid_trumps_permit— if any forbid policy is satisfied, the request is denied. -
allowed_only_if_explicitly_permitted— a request is allowed only if at least one permit policy is satisfied. -
typecheck_is_sound— if the validator accepts a policy, evaluation produces a boolean.
Cedar — The Engineering Story
Executable Lean model alongside Rust production code. Lean model ~10× smaller than Rust.
-
~100M differential random tests nightly. Lean: 5 μs/test. Rust: 7 μs/test.
-
Release gate: no Cedar version ships unless model, proofs, and differential tests are current.
"We've found Lean to be a great tool for verified software development." — Emina Torlak
SampCert (AWS): Verified Differential Privacy
An open-source Lean library of formally verified differential privacy primitives.
The implementation is not only verified, but it is also twice as fast as the previous one.
SampCert is software, but its verification relies heavily on Mathlib.
The verification of code addressing practical problems in data privacy depends on the formalization of mathematical concepts, from Fourier analysis to number theory and topology.
Deployed in AWS Clean Rooms Differential Privacy.
PLDI 2025: "Verified Foundations for Differential Privacy."
“For SampCert, I started using Lean because of Mathlib, but I realized that Lean isn't just an excellent proof assistant, it's also a very pleasant and efficient programming language with a great ecosystem.” — Jean-Baptiste Tristan
Strata (AWS): Language Syntax and Semantics
Strata: extensible platform for formalizing language syntax and semantics. Built in Lean. Open source.
Key idea: dialects (inspired by MLIR). Orthogonal, composable building blocks for modeling programming constructs.
-
Core, C_Simp, Laurel, SMTLib, Python, Boole.
-
Laurel pipeline: Python/Java/JavaScript → Laurel → Strata Core → VCG → SMT.
-
Dialect Definition Mechanism (DDM): embedded DSL in Lean for defining syntax and typing rules.
-
Boogie/Dafny-style verification infrastructure, built in Lean and extensible via Lean's metaprogramming.
Waimea (AWS): Verified Compiler for Trainium
CompCert-style verified compiler for AWS Trainium, Amazon's custom AI accelerator chip. ~500,000 lines of Lean code.
-
The ISA specification changes several times per week. Not a fixed ISA like x86.
-
Lean provides an up-to-date simulator that hardware and verification engineers share.
-
Lean + AI keeps the team in sync with hardware changes. Several hundred instructions per generation.
-
Used to find hardware and simulator bugs and prove the correctness of subtle hardware optimizations.
Long-term goal: end-to-end compiler verification — source program compiles to Trainium machine code, with a proof that compilation preserves semantics.
"Lean is a fantastic functional programming language." — Sean McLaughlin
SymCrypt (Microsoft): Verified Cryptography
SymCrypt — Microsoft's core cryptographic library, rewritten in Rust.
Aeneas: translates safe Rust to pure functional Lean code.
The first release includes complete proofs for ML-KEM and SHA-3 code running in Windows Insider builds today.
"We are verifying code faster than we can write it." — Son Ho, SymCrypt, Microsoft
Veil: Verified Distributed Protocols
Veil: verification of distributed protocols. Built on Lean as a library using Lean metaprogramming.
"Multi-Modal Verification of Distributed Systems in Lean" — Ilya Sergey
-
Authors: George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey.
-
Push-button verification via SMT (cvc5/Z3) for decidable fragments.
-
Full interactive proofs in Lean when automation falls short.
-
Seamless transition between the two modes.
-
Foundational: Veil's VCG is proven sound w.r.t. the specification language semantics.
-
16 distributed protocol case studies. All 16 verified. Ivy failed on 2. 87.5% verified in under 15 seconds.
Kraken (Google): x64 Semantics in Lean
Jonathan Protzenko and Andres Erbsen
Kraken: the x64 model is intended for verifying sequential software that performs computations using common registers and memory.
A semantics optimized for proof automation.
Uses lessons learned from Bedrock2 — the interpreter either computes a WP or a final state.
Currently supports x64, arm64 (WIP), and RISC-V (on the roadmap).
Current status: pre-alpha; tactics still need Lean support to get to the level required to prove non-trivial programs.
Project started after the Lean@Google Hackathon in December 2025.
Move Borrow Checker
Ilya Sergey (VERSE lab) formalized and verified Move's borrow checker in Lean. 39,000 lines of mechanized metatheory in 27 working days, using Claude as an AI coding assistant.
Move: smart contract language for the Sui and Aptos blockchains. Rust-like ownership discipline. References are access paths rooted in local variables. No lifetime annotations.
The borrow checker: tracks reachability between references using regular expressions over field paths.
Formalized in Lean:
-
Relational type system encoding
-
Executable algorithmic type checker
-
Soundness proof: the algorithmic checker is sound w.r.t. the relational rules
-
Runtime semantics as a definitional interpreter
-
Type soundness: progress + preservation. Any function accepted by the type checker never reaches a preventable error across all execution paths.
CSLib: A Mathlib for Computer Science
CSLib aims to be a foundation for teaching, research, and new verification efforts, including AI-assisted.
Steering committee: Clark Barrett, Swarat Chaudhuri, Jim Grundy, Pushmeet Kohli, Leo de Moura, Fabrizio Montesi.
Iris Lean
Iris is a higher-order concurrent separation logic framework implemented in Rocq.
Very popular. 150+ papers since 2015.
Iris Lean is a port of Iris to Lean. Progress (last week): 70.3%
Started as Lars König's master's thesis (2022). Maintained by Mario Carneiro until 2025; then Markus de Medeiros and many others got interested.
Introduction to Iris-Lean by Zongyuan Liu. Why port Iris to Lean? Zongyuan's answer:
Signal Shot
Signal Shot is a public moonshot to verify the Signal protocol and its Rust implementation using Lean.
It is a joint effort of Signal (Rolfe Schmidt), the Beneficial AI Foundation (Max Tegmark), and the Lean FRO.
The pieces:
-
Aeneas
-
Mathlib and CSLib
-
Symbolic proof automation (
grind) and scalable verification generation (SymM) -
AI
VC Generation & Scalability
A VC generator turns code and specifications into proof obligations. Lean-based VC generators:
-
Aeneas — Rust verification via translation to Lean.
-
Velvet — a Dafny-style verifier built in Lean.
-
vcgen — Lean's VC generator for monadic programs.
Issue: Verification condition generation with proof assistants has not scaled so far.
Adam Chlipala's group documented this for Rocq. The same story held in Lean until a few months ago.
Andres' Challenge
Andres Erbsen — Google ISE Formal. Bedrock2. Fiat Cryptography.
A Rocq veteran distilled the scaling problem into a minimal challenge at Lean@Google Hackathon.
A parametric example for a small deeply embedded imperative language.
With Lean's default tactic framework, MetaM, this is superlinear.
What Must Be Fast in VC Generation
A VC generator turns code and specifications into proof obligations.
Lean-based VC generators: Aeneas, Velvet, vcgen.
All three share the same idiom — and need:
-
Efficient
apply. -
Efficient metavariable management.
-
Preserve term sharing.
-
Reuse
simpandgrindresults across proof obligations and across simulation steps. -
Do not traverse the same subterms over and over.
SymM: Scalable Symbolic Verification
-
SymM: new monadic framework for high-performance software verification. Born after the Lean@Google Hackathon. -
Designed for tools like Aeneas, vcgen, and Velvet that need to discharge thousands of verification conditions efficiently.
Without this, verifying something as large as Signal is slow and painful. With it, verification conditions get discharged efficiently.
vcgen — Ported to SymM
Lean's VC generator for monadic programs. Ported to SymM by Sebastian Graf (Lean FRO).
Andres' Challenge using Lean monadic code. Linear out to n=1000.
Velvet — Ported to SymM
A Dafny-style verifier in Lean. Ported to SymM by Vova (VERSE lab and Lean FRO intern). Preliminary results.
-
Before: Velvet ran ~3× slower than Dafny.
-
After: Faster than Dafny on 24 of 27 benchmarks; competitive on the other 3 (
differenceMinMax,findEvenNumbers,mergeSorted).
The new version beats Dafny on 24 of 27. Dafny has a vast TCB.
DyLean — Cryptographic Protocols
A Lean framework by Théophile Wallez for proving the security of cryptographic protocols.
The proof methodology builds on (and improves) DY*.
DyLean leverages grind to discharge preconditions: automation on par with DY* / F* (which use Z3).
SymM + incremental grind in the VC generator led to a 50× speedup.
bv_decide — Ported to SymM
Lean's bit-vector decision procedure. Ported to SymM by Henrik Böving (Lean FRO).
Benchmarked against Bitwuzla on 46,191 SMT-LIB bit-vector problems.
-
bv_decidesolves 45,046 (97.5%) — kernel checking included. Bitwuzla solves 45,817. -
Identical sat/unsat verdicts on every problem both solved.
-
Total CPU time within 2.3× of Bitwuzla.
Amazon is investing in the Lean FRO
Accelerate Lean’s development as both a software verification platform and a programming language.
The single largest donation in the Lean FRO's history. Substantial, long-term support.
"It's easier to trust a proof when the tools that check it are open." — Byron Cook and Shawn Bice
Community-governed tools can be inspected and validated independently by customers, auditors, and regulators.
The Automated Reasoning Group at AWS is hiring!
Conclusion
Lean is extensible, scalable, and trusted, with great tooling.
The Mathlib community is changing how mathematics is done.
Lean is not only for mathematics. Software verification is now a major use case.
Specification-oriented development is within reach.
New libraries: CSLib, Physlib.
AI is bringing formal verification to everyone.
The Lean FRO Year 4 roadmap is coming soon: many new features and optimizations in the pipeline.
AI changes how we build proof assistants. It does not change what makes them good.
Formal methods has never been more relevant.