The Lean Theorem Prover: Design, Evolution, and Impact

The Lean Theorem Prover, an open-source proof assistant and programming language, has reached 280,000+ formalized theorems and 2.4M+ lines of code with 750+ contributors as of July 2026, according to Kim Morrison. Lean 4.0, released officially in September 2023, features a small trusted kernel and extensible design, enabling AI-assisted formal verification that makes AI trustworthy and cost-effective. The Lean FRO, a nonprofit with 20 engineers launched in July 2023, has shipped 32 releases and merged 9,000+ pull requests, with the project featured in NY Times, Quanta, and Scientific American.

Formal verification makes AI trustworthy. AI makes formal verification cost-effective. Hex https://github.com/leanprover/hex is a Lean https://lean-lang.org 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 https://kim-em.github.io/blog/2026-7-7-lattice-basis-reduction-using-the-hex-lean-library/ 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. "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 := byn:Nat⊢ odd n → odd n n intro ⟨k₁, e₁⟩n:Natk₁:Nate₁:n = 2 k₁ + 1⊢ odd n n simp e₁, odd n:Natk₁:Nate₁:n = 2 k₁ + 1⊢ ∃ k, 2 k₁ + 1 2 k₁ + 1 = 2 k + 1 exists 2 k₁ k₁ + 2 k₁n:Natk₁:Nate₁:n = 2 k₁ + 1⊢ 2 k₁ + 1 2 k₁ + 1 = 2 2 k₁ k₁ + 2 k₁ + 1 liaAll goals completed 🐙 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. 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" https://dl.acm.org/doi/10.1145/3110278 — ICFP 2017. This design made community automation possible: linarith , ring , omega , and hundreds more. The community implemented several linters in Lean. Created in July 2017, in Lean 3 during Big Proof https://www.newton.ac.uk/event/bpr/ . 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 Sebastian Ullrich https://sebasti.a.nullri.ch/ 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 . 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 Nonprofit. 20 engineers. Open source. Controlled by no single company. Sebastian Ullrich https://sebasti.a.nullri.ch/ 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. 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 https://marketplace.visualstudio.com/items?itemName=leanprover.lean4 161K + Open VSX https://open-vsx.org/extension/leanprover/lean4 126K . def reverse : List α → List α | = | x :: xs = reverse xs ++ x theorem reverse append xs ys : List α : reverse xs ++ ys = reverse ys ++ reverse xs := byα:Type u 1xs:List αys:List α⊢ reverse xs ++ ys = reverse ys ++ reverse xs induction xs with | nil = α:Type u 1ys:List α⊢ reverse ++ ys = reverse ys ++ reverse simp reverse All goals completed 🐙 | cons x xs ih = α:Type u 1ys:List αx:αxs:List αih:reverse xs ++ ys = reverse ys ++ reverse xs⊢ reverse x :: xs ++ ys = reverse ys ++ reverse x :: xs simp reverse, ih All goals completed 🐙 eval 3, 2, 1 reverse 1, 2, 3 3, 2, 1 Instructions to build Mathlib, measured for every commit by radar https://radar.lean-lang.org , 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. Six Fields Medalists engaged: Tao, Scholze, Viazovska, Gowers, Hairer, Freedman. Carleson's Theorem https://florisvandoorn.com/carleson// completed — van Doorn Liquid Tensor Experiment https://www.nature.com/articles/d41586-021-01627-2 completed — Commelin The Polynomial Freiman-Ruzsa Conjecture https://github.com/teorth/pfr , Tao completed Equational Theories Project https://teorth.github.io/equational theories/ , Tao completed Sphere Packing https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/ — Birkbeck, Hariharan, Lee, Ma, Mehta, Viazovska Fermat's Last Theorem https://leanprover-community.github.io/blog/posts/FLT-announcement/ — Buzzard Inter-Universal Teichmüller Theory https://aitpm.github.io/slides/Mochizuki.pdf — Mochizuki At this scale, mathematics needs build systems, dependency graphs, code review, release engineering, and a precise medium for communication. 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. Future math papers will embed type-checked Lean code. Lecture notes, papers, and slides in one tool. These slides are written in Verso https://verso.lean-lang.org/ . Every example is checked by Lean. lean-lang.org https://lean-lang.org/ is written in Verso. My homepage https://leodemoura.github.io/ is written in Verso. Verso is a domain-specific language embedded in Lean. Built by David Thrane Christiansen at the Lean FRO. Verso Blueprint is the next generation of Massot's Lean Blueprints https://github.com/PatrickMassot/leanblueprint , 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 provides natural-language tactics to teach mathematics using Lean 4. Playing the Lean game using mouse clicks and natural language. Lean Verbose https://github.com/PatrickMassot/verbose-lean4 is implemented in Lean by Patrick Massot. 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. 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 Lean checks them. 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 https://borisalexeev.com/pdf/erdos707.pdf 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. 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. Sidharth Hariharan and collaborators describe how Viazovska's Fields Medal-winning sphere packing proofs were formally verified in Lean https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/ . "They Spent Years on a Math Problem. Then They Were Scooped by A.I." — NY Times https://www.nytimes.com/2026/06/08/science/ai-scoop-young-mathematicians.html "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 . 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 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. A Mathlib Initiative https://mathlib-initiative.org/formal-frontier/ 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. 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 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. Public results on a benchmark of hard Lean formalization problems. Submission-based leaderboard. Erdős's unit-distance conjecture is one of the problems https://lean-lang.org/eval/problems/erdos unit distance conjecture false/ . 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 https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/ Feit–Thompson odd-order theorem https://lean-lang.org/eval/problems/feit thompson/ — 4 submissions Jacobian of a compact Riemann surface Buzzard challenge https://lean-lang.org/eval/problems/jacobian challenge diffgeo/ — 4 submissions Formal Conjectures https://google-deepmind.github.io/formal-conjectures/ Google DeepMind : curated, human-verified formal statements of open problems. "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 https://arena.lean-lang.org . Validating a Lean Proof https://lean-lang.org/doc/reference/latest/ValidatingProofs/ validating-proofs ∣ Who Watches the Provers? https://leodemoura.github.io/blog/2026-3-16-who-watches-the-provers/ arena.lean-lang.org https://arena.lean-lang.org benchmarks independent proof checkers on the same proofs. Comparator https://github.com/leanprover/comparator is a judge for Lean proofs. comparator.live.lean-lang.org https://comparator.live.lean-lang.org/ Avoids metaprogramming / unsafe exploits. Exports proofs. Sandboxed. A challenge is a Lean file with sorry s to be filled. def large : Nat := sorry theorem large lt : 37 < large := sorry A solution replaces the sorry s with Lean terms and proofs. def large : Nat := 38 theorem large lt : 37 < large := by⊢ 37 < large decideAll goals completed 🐙 Comparator checks whether the solution is valid. 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 https://github.com/leanprover/lean4/issues/14484 . 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. "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. 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+ grind uses 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α:Type u 1inst✝¹:CommRing αinst✝: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 grindAll goals completed 🐙 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. 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α:Type u 1inst✝²:CommRing αinst✝¹:IsCharP α 0inst✝: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 grindAll goals completed 🐙 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 . 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 https://github.com/plclub/sf-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 https://imo-grand-challenge.github.io/ 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. Lean is not only for mathematics. Cedar https://www.cedarpolicy.com/en — open-source authorization policy language. Used by AWS Verified Permissions and AWS Verified Access . Cedar spec https://github.com/cedar-policy/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. 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 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 https://strata-org.github.io/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. 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 https://www.microsoft.com/en-us/research/blog/rewriting-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library/ — 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 https://veil.dev/ : 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. Jonathan Protzenko https://jonathan.protzenko.fr/ and Andres Erbsen https://andres.systems/ Kraken https://github.com/AeneasVerif/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 https://sites.google.com/view/lean-at-googl-2025/home in December 2025. 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 https://www.cslib.io/ 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 https://iris-project.org/ is a higher-order concurrent separation logic framework implemented in Rocq. Very popular. 150+ papers since 2015. Iris Lean https://leanprover-community.github.io/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 https://www.youtube.com/watch?v=1TPmpuRaTvc . Why port Iris to Lean? Zongyuan's answer: Signal Shot https://www.beneficialaifoundation.org/blog/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 https://www.beneficialaifoundation.org/ Max Tegmark , and the Lean FRO. The pieces: Aeneas Mathlib and CSLib https://www.cslib.io/ Symbolic proof automation grind and scalable verification generation SymM AI 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 Erbsen — Google ISE Formal. Bedrock2. Fiat Cryptography. A Rocq veteran distilled the scaling problem into a minimal challenge at Lean@Google Hackathon https://hackmd.io/sjPWIMP9TIuKW5tuWUfxXA . A parametric example https://github.com/leanprover/lean4/blob/master/tests/bench/sym/add sub cancel.lean for a small deeply embedded imperative language. With Lean's default tactic framework, MetaM , this is superlinear . 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 simp and grind results across proof obligations and across simulation steps. Do not traverse the same subterms over and over. SymM : new monadic framework for high-performance software verification. Born after the Lean@Google Hackathon https://hackmd.io/sjPWIMP9TIuKW5tuWUfxXA . 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. 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. 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. 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 decide solves 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. 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 Lean https://lean-lang.org/ 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 https://www.cslib.io/ , Physlib https://physlib.io/ . 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.