Why Lean?
What is Lean?
-
A programming language and a proof assistant. Same language for code and proofs.
-
Small trusted kernel. Multiple independent kernels. Proofs can be exported and independently checked.
-
Implemented in Lean. Very extensible.
-
Open source. Lean FRO — Nonprofit. Controlled by no single company.
Lean Is Taking Mathematics by Storm
Five Fields Medalists engaged: Tao, Scholze, Viazovska, Gowers, Hairer.
-
Mathlib: 200,000+ theorems, 750+ contributors, 2.2M+ LoC
-
Liquid Tensor Experiment: verified a proof Scholze himself had "lingering doubts" about.
-
Equational Theories Project — Terence Tao
-
Fields Medal sphere packing — AI assisted
-
Fermat's Last Theorem — Kevin Buzzard
The same platform that Fields Medalists use for cutting-edge mathematics is the platform you'll use to verify Signal's cryptographic proofs.
The math infrastructure is already there.
No Reward Hacking
"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
The kernel's soundness is AI safety infrastructure.
-
Multiple independent kernels. arena.lean-lang.org
-
You don't need to trust us, or our proof automation. You only need to trust the small kernel, and we have several.
The same trust model you want for your protocol — no single point of failure, independently verifiable — is how Lean proofs work.
zlib: AI Proved It Correct
A general-purpose AI, with no special training for theorem proving, converted zlib (a C compression library) to Lean, passed the test suite, and then proved that the code is correct.
theorem zlib_decompressSingle_compress (data : ByteArray) (level : UInt8)
(hsize : data.size < 1024 * 1024 * 1024) :
ZlibDecode.decompressSingle (ZlibEncode.compress data level) = .ok data
Decompression always recovers the original data. Every compression level. Machine-checked.
The barrier is no longer AI capability. It is platform readiness.
Signal Shot will use AI + Lean the same way: translate Rust via Aeneas, then prove correctness.
lean-zip | When AI Writes the World's Software, Who Verifies It?
Software Verification: Aeneas, SymCrypt, Veil, Velvet
-
Aeneas (Son Ho, Microsoft): Rust → Lean translation. The bridge for Signal. Verified Rust code as written by software engineers.
-
SymCrypt (Microsoft): Core cryptographic library, verified using Aeneas + Lean.
-
Cedar (AWS): Authorization policy engine. Verified in Lean.
-
Veil (Ilya Sergey): Verified distributed protocols.
These are not future plans. These tools exist and are being used today.
SymM + grind: Making Verification Scale
-
grind: SMT-inspired tactic. Native to dependent type theory. -
SymM: new monadic framework for high-performance software verification. Born after the Lean@Google Hackathon last December. -
Designed for tools like Aeneas, mvcgen 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.
-
AI replaces heuristics. The algorithmic core is more valuable than ever. Proof Assistants in the Age of AI
Why Lean?
-
Open source. Nonprofit. Controlled by no single company.
-
Lean FRO: 20 engineers advancing Lean for the future.
-
The ecosystem: 8,000+ GitHub repos, 200,000+ VS Code + Open VSX unique installs.
-
Every AI system that solved IMO problems with formal proofs used Lean. No competing platform.
-
AI startups using Lean: Axiom, Harmonic, Logical Intelligence, Math Inc, Mistral
-
CSLib: a Mathlib for computer science.
-
ACM SIGPLAN Award 2025: "Lean has become the de facto choice for AI-based systems of mathematical reasoning."
Lean is where the math, the tools, scalable verification, the AI, and the community already are.
Let's do it! Signal Shot will be the Liquid Tensor Experiment of Software Verification.