Lean 4 beyond research
A snapshot, taken at the start of the Fall 2026 semester, of organizations using Lean 4 outside of research: what each one is doing with it, and the scale of the organization doing it. Every figure and claim is cited on the snapshot page, whose numbers link through to all thirty sources.
| Organization | Valuation | Lean 4 work | Emphasis |
|---|---|---|---|
| Google DeepMind / Alphabet | Alphabet $4.13T | AlphaProof — reinforcement learning over Lean; olympiad-level formal reasoning, published in Nature | Autoformalization |
| Microsoft | $3.69T | Originated Lean. Aeneas-based Lean verification of Rust SymCrypt, with ML-KEM and SHA-3 proofs shipping in Windows Insider builds | Verified production |
| Amazon / AWS | $2.75T | Cedar authorization language, modelled in Lean and differentially tested against the production Rust; the proofs found 4 validator bugs and testing found 21 more | Verified production |
| Anthropic | $965B | Claude raised a lower bound on zeta zeros from 41.6% to 67.2%, with a Lean formalization that passes the standard validation tool | New mathematics |
| OpenAI | $852B | Ten decade-open problems, each shipped with a machine-checkable Lean 4 certificate | New mathematics |
| ByteDance | >$600B | BFS-Prover — best-first search over Lean 4, open-sourced; 72.95% on MiniF2F | Theorem proving |
| Tencent | $503B | HunyuanProver — data synthesis at scale with guided tree search | Theorem proving |
| DeepSeek | ~$74B | DeepSeek-Prover-V2 — subgoal decomposition by reinforcement learning; 88.9% on MiniF2F-test | Theorem proving |
| Moonshot AI | ~$50B | Kimina-Prover, built with Project Numina | Theorem proving |
| Mistral AI | ~$23B | Leanstral — the first open-source code agent designed for Lean 4, Apache 2.0 | Autoformalization |
| Harmonic | $1.45B | Aristotle — formally verified gold-medal-level performance at IMO 2025 | Autoformalization |
| Math, Inc. | Undisclosed | Gauss completed the Tao–Kontorovich challenge to formalize the strong Prime Number Theorem in Lean; OpenGauss released MIT-licensed | Autoformalization |
| Huawei | Employee-owned | Mathesis — natural language to Lean 4 via an RL-trained autoformalizer | Autoformalization |
| Nethermind | Private | EVM and Yul semantics in Lean, passing 99.99% (22,330/22,332) of the Cancun execution tests; Halva found a Keccak-256 bug in Scroll’s circuit | Verified production |
| Galois | Private | FVSpec — 2,772 property-based tests translated into 9,415 Lean 4 specifications | Verified production |
Market capitalizations retrieved 2 September 2026, in USD; private valuations are the most recent round, and some were still open at that date. Each claim above is cited on the snapshot page, whose figures link through to all thirty sources.