Lean 4 and Mathlib: The proof assistant the ZK verification ecosystem has standardised on
================================================================================

Lean 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: Clean, zkLean, Halva, ArkLib, sp1-lean, Lampe, EvmYul, Cairo 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: Active
Strengths: De facto standard for ZK proofs. | Mathlib depth for field and polynomial arithmetic. | Best AI-assistant support of any prover.
Limits: Proof engineering cost. | Fast-moving toolchain; pin versions. | Trusted axioms must be audited per project.
Firms using it: zkSecurity, Galois, Nethermind (Formal Verification team), Reilabs
Sources: https://lean-lang.org | https://blog.zksecurity.xyz/posts/introduction-to-interactive-theorem-provers/

Source page: https://sorryfree.com/frameworks/lean4/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13