Lean 4, Fall 2026

Originated Lean. Aeneas-based Lean verification of Rust SymCrypt: "complete proofs for the Rust ML-KEM and SHA3 code that is being used in insiders builds of Windows today"¹³

Cedar authorization language, modelled in Lean and differentially tested against the production Rust¹⁴; the proofs found 4 validator bugs and testing found 21 more¹⁵

EVM and Yul semantics in Lean, "passing 99.99% (22,330/22,332) of these Cancun execution tests"²⁷; Halva found a Keccak-256 bug in Scroll's circuit²⁸

FVSpec — 2,772 property-based tests translated into "9,415 Lean 4 specifications"²⁹; released under the GaloisInc organization³⁰

BFS-Prover — best-first search over Lean 4, open-sourced; 72.95% on MiniF2F¹⁸

HunyuanProver — scalable data synthesis with guided tree search for automated theorem proving¹⁹

DeepSeek-Prover-V2 — subgoal decomposition by reinforcement learning; 88.9% on MiniF2F-test²⁰

Kimina-Prover — "developed by Project Numina and Kimi teams … in Lean 4"²¹

AlphaProof — reinforcement learning over Lean; olympiad-level formal reasoning, published in Nature¹²

Leanstral — "the first open-source code agent designed for Lean 4", weights under Apache 2.0, evaluated on the Fermat's Last Theorem project²²

Aristotle — "among the first AI models to achieve formally verified gold medal-level performance on the 2025 International Mathematical Olympiad"²³

Gauss completed "a challenge set by Fields Medallist Terence Tao and Alex Kontorovich … to formalize the strong Prime Number Theorem (PNT) in Lean"²⁴; OpenGauss released MIT-licensed²⁵

Mathesis — natural language to Lean 4 via an RL-trained autoformalizer²⁶

Claude raised a lower bound on zeta zeros "from 41.6% to 67.2%"; the Lean formalization "passes the standard validation tool comparator"¹⁶

Public repository of "Lean certificates accompanying ten proofs in mathematics and theoretical computer science"¹⁷