Lean 4 and Mathlib
Direct answerLean 4 is the proof assistant behind nearly every ZK verification project funded in 2025 and 2026: Clean, zkLean, Halva, ArkLib, sp1-lean, Lampe, proven-zk, Nethermind's EVM model and StarkWare's Cairo proofs. Mathlib supplies the finite-field and polynomial mathematics, and AI proving tools now target it.
- Maintainer
- Lean FRO and the Mathlib community
- Website
- https://lean-lang.org
- Category
- Proof assistants and general verifiers
- Targets
- CleanzkLeanHalvaArkLibsp1-leanLampeEvmYulCairo AIR proofs
- Approach
- Interactive theorem prover with a small trusted kernel, a large mathematics library and a growing AI-prover ecosystem
- Access
- Open source (Apache-2.0)
- Status (2026-09-13)
- Active
What Lean 4 and Mathlib does
Choosing Lean fixes the hiring pool, the reusable libraries and the interoperability with everything else on this index. The kernel is small; the axioms a project uses (and whether it relies on native_decide) are the things to check when reading a Lean result, which is why zk.golf enforces an axiom allowlist.
Where it is strong
- De facto standard for ZK proofs.
- Mathlib depth for field and polynomial arithmetic.
- Best AI-assistant support of any prover.
Limits and caveats
- Proof engineering cost.
- Fast-moving toolchain; pin versions.
- Trusted axioms must be audited per project.
When to choose it
Default choice for any new circuit or proof-system verification.
Who works with Lean 4 and Mathlib
zkSecurity, Galois, Nethermind (Formal Verification team), Reilabs.
Top-listed for proof engineering work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Related frameworks in Proof assistants and general verifiers
Rocq (formerly Coq), Isabelle/HOL, F*, ACL2 (R1CS and PFCS books), K framework and KEVM, Certora Prover.