💡 왼쪽 원문을 읽으면서 오른쪽에 따라 써보세요. Tab 키로 힌트를 받을 수 있습니다.

원문 렌더가 준비되기 전까지 텍스트 가이드로 표시합니다.

1. A map of proof assistants in 2026 — six camps

In 2026, the proof-assistant (theorem-prover) ecosystem is more alive than it has ever been. Tools that were called "toys for mathematicians" a decade ago are now **the daily notebooks of the world's top mathematicians** and **the safety certificates of OS kernels and crypto libraries**.

The major living camps right now:

| --- | --- | --- | --- |

On top of these seven, two currents are reshaping the air of 2026:

1. **AI assistance** — DeepMind's AlphaProof scored a silver-medal-level result at IMO 2024 (4 of 6 problems, 28/42 points), and Anthropic joined the AI Mathematical Olympiad ($5M prize) plus mathlib search and auto-proving. Claude- and GPT-class LLMs are now routinely used as Lean tactic generators.

2. **First-rank mathematicians joining** — Terence Tao (Fields Medal 2006) is publicly formalising his own papers (e.g. the PFR conjecture) in Lean; Kevin Buzzard (Imperial College) argues in public lectures that "every undergraduate mathematician should learn Lean."

This post takes those seven camps one at a time, then the AI, SMT, and industrial-verification stories in turn.

> **Terminology**: a proof assistant is a tool where a human writes a proof and the computer checks every line. An SMT solver is a back-end engine that automatically decides whether a formula is satisfiable (Z3, CVC5). When you fuse them, you get F\* or Liquid Haskell, where ordinary code is verified.

2. Lean 4 — Leonardo de Moura, AWS, explosive growth

A short history of Lean

Lean started at Microsoft Research in 2013 under **Leonardo de Moura** (yes, the same author as Z3). It went through Lean 2 (2015) and Lean 3 (2017), and Lean 4 stabilised in 2021. In 2023, de Moura left Microsoft to join **Amazon Web Services'** Automated Reasoning Group. AWS now funds Lean 4 compiler development and mathlib infrastructure.

What Lean 4 is

Lean 4 is not just a proof assistant. It is **a full dependently-typed functional programming language**.

-- Commutativity of natural-number addition

theorem add_comm (a b : Nat) : a + b = b + a := by

induction b with

| zero => simp

| succ b ih => rw [Nat.add_succ, ih, Nat.succ_add]

`theorem` declares a proposition; `:=` introduces its proof. Inside a `by ... ` block you call tactics like `induction`, `simp`, and `rw` (rewrite) to discharge the current goal step by step.

Why Lean 4 is fast

- **Self-hosting compiler** — Lean 4 is written in Lean and compiled to C, so it runs at native speed.

- **Macro system** — Racket-style macros let users build domain-specific syntax. mathlib uses this so that mathematical notation reads as itself.

- **Type classes** — Haskell-style type classes make abstractions clean.

Install and your first proof

elan: the Lean version manager (think rustup)

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

A new project

lake new my_first_lean

cd my_first_lean

lake build

Install the VS Code Lean 4 extension and hover with your mouse to see the current goal and types live. That InfoView is the first thing Lean users fall in love with.

Status in 2026

- Lean 4.10+ stable

- mathlib past one million theorems (see next chapter)

- Adopted in undergrad: Imperial College, Brown, Berkeley, CMU

- Industry: AWS Automated Reasoning, Galois, Kestrel Institute

> The Lean Community site [leanprover-community.github.io](https://leanprover-community.github.io/) and the [Zulip chat](https://leanprover.zulipchat.com/) are practically alive 24/7. Post a question and someone usually answers within an hour.

3. mathlib — one million theorems, Terence Tao's notebook

What mathlib is

**mathlib4** (for Lean 4) is the largest formalised mathematics library in human history. As of May 2026:

- **1,000,000+ theorems / lemmas / defs combined** (crossed early 2026)

- Roughly 300k lines of definitions, 800k lines of proofs

- 600+ contributors in `git log`

- Groups, rings, fields, topology, measure, categories, analysis, algebraic geometry — essentially the entire undergrad-to-grad curriculum

Structure and notation

-- Real analysis: monotonicity of the integral

theorem integral_mono (f g : ℝ → ℝ)

(hf : Integrable f) (hg : Integrable g)

(h : ∀ x, f x ≤ g x) :

∫ x, f x ≤ ∫ x, g x := by

exact MeasureTheory.integral_mono hf hg h

Writing in nearly the same notation as ordinary mathematics is the heart of mathlib. `ℝ`, `∫`, `≤` are just Unicode characters. Lean 4's macro system makes it work.

Terence Tao and the PFR Project

In November 2023, Terence Tao (Fields Medal) — together with Tim Gowers, Ben Green, and Freddie Manners — kicked off a project to formalise their proof of the [Polynomial Freiman-Ruzsa conjecture](https://arxiv.org/abs/2311.05762) in Lean in three weeks. He documented the whole thing publicly on his blog `terrytao.wordpress.com`.

The headline: **"formalisation now takes a mathematician under a month, and AI is doing more and more of it."**

As of 2026 Tao has started writing parts of his new papers directly in Lean from the start.

Who contributes to mathlib

- Imperial College (Kevin Buzzard's group)

- Brown University (Heather Macbeth)

- Carnegie Mellon (Jeremy Avigad)

- Many PhD students, undergraduates, and hobbyist mathematicians

- Increasingly, AI assistance (next chapters)

Your first PR

mathlib has a low entry barrier. There is a [contribute page](https://leanprover-community.github.io/contribute/index.html) for new contributors. One theorem, one definition, or one auxiliary lemma is welcome.

4. Rocq (ex-Coq, rebranded March 2024) — 25 years of classic

Why the name changed

In March 2024, the Coq dev team announced in [this thread](https://coq.discourse.group/t/coq-renaming-from-coq-to-rocq/2243) that **Coq would be rebranded as Rocq**. Two reasons:

1. The word "Coq" sounds vulgar in some languages, creating a barrier for newcomers.

2. A new-generation identity — as Lean was drawing users away, it was time to redefine the project itself.

The domain moved through `coq.inria.fr` to [`rocq-prover.org`](https://rocq-prover.org/). The codebase itself carries on 25 years of history unchanged (Coq 1.0 dates to 1989).

Rocq's strengths

- **Strong industrial-verification record** — CompCert (below), seL4 auxiliaries, Verdi (distributed systems), CertiCrypt, Iris, and more

- The **Coq Standard Library** is very stable

- **Ssreflect / mathcomp** — the proof-strategy library Georges Gonthier built while formalising the Four Color Theorem and the 255-page Feit-Thompson theorem. Older than mathlib.

- **OCaml-based** — tightly bound to INRIA's OCaml ecosystem

A short Rocq snippet

Theorem add_comm : forall a b : nat, a + b = b + a.

Proof.

intros a b.

induction a as [| a' IH].

- simpl. rewrite <- plus_n_O. reflexivity.

- simpl. rewrite IH. rewrite plus_n_Sm. reflexivity.

Qed.

`intros`, `induction`, `simpl`, `rewrite`, `reflexivity`. The shape looks like Lean but the syntax is more Lispy (closed with `Qed.`).

Rocq vs Lean in 2026

| Aspect | Rocq | Lean 4 |

| --- | --- | --- |

| History | 1989~ | 2013~ |

| Library | mathcomp, stdlib | mathlib (1M+) |

| Adoption | flat / declining | explosive |

| Industry | CompCert, ProofGeneral | AWS Automated Reasoning |

| Entry difficulty | steep | steep, but the Lean Game exists |

Rocq is not dead — 25 years of industrial code isn't going anywhere, and INRIA plus many universities still back it strongly.

5. Agda — the canonical dependent-type language

Where Agda sits

Agda comes out of Chalmers (Sweden) and is **a pure dependently-typed functional language**. Compared to Lean, its identity as a programming language is stronger — all functions must terminate (totality check), and there is essentially no distinction between types and values.

Agda's notation — a Unicode paradise

data ℕ : Set where

zero : ℕ

suc : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ

zero + n = n

suc m + n = suc (m + n)

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m

+-comm zero n = sym (+-identity n)

+-comm (suc m) n = trans (cong suc (+-comm m n)) (sym (+-suc n m))

`ℕ`, `≡`, `∀`, `→` — all Unicode. The Emacs/VS Code Agda mode converts `\to`, `\equiv`, `\forall` as you type.

Agda strengths

- **Types and values are fully identified** — one step purer than Lean

- **Cubical Agda** — the standard implementation of Homotopy Type Theory

- **PLFA** ([Programming Language Foundations in Agda](https://plfa.github.io/)) — arguably the best PL-foundations textbook of its kind

Agda weaknesses

- No large standard library (`agda/stdlib` exists but is dwarfed by mathlib)

- Almost no industrial adoption

- Automation (tactics) is very weak — proofs are mostly manual

Should you learn Agda in 2026?

If the goal is **type theory study**, **HoTT research**, or **PL research**, yes. If the goal is industrial verification or a large maths library, Lean 4 is better.

6. Idris 2 — Edwin Brady's practical dependent types

Idris 2's identity

Idris was built in St Andrews (UK) by **Edwin Brady**. Idris 1 (2011) was a Haskell-written academic prototype; **Idris 2** (2020 onward) is self-hosted in Idris and crucially adopts **Quantitative Type Theory** (QTT, due to Bob Atkey).

Idris 2's core — quantitative types

data List : (a : Type) -> Type where

Nil : List a

(::) : a -> List a -> List a

length : List a -> Nat

length [] = 0

length (_ :: xs) = 1 + length xs

-- Index that exists only at compile time (quantity 0)

data Vect : Nat -> Type -> Type where

Nil : Vect 0 a

(::) : a -> Vect n a -> Vect (S n) a

QTT assigns each argument a quantity of **0 / 1 / many**. `0` means compile-time only, `1` means exactly once, `many` is an ordinary variable. This unifies dependent types and linear types.

What Idris 2 aims for

Idris is the most directly aimed at "dependent types for programming." Lean leans toward mathematics and Agda toward PL theory, while Idris keeps **actual software development** in mind.

- Downside: small community, few libraries

- Upside: Brady's book [*Type-Driven Development with Idris*](https://www.manning.com/books/type-driven-development-with-idris) is the standard intro to dependent types

7. Isabelle/HOL — the tool that proved seL4

Isabelle's identity

Isabelle has been developed since 1986 by Larry Paulson (Cambridge) and Tobias Nipkow (TUM). It uses **classical HOL (Higher-Order Logic)** rather than the constructive logic plus dependent types of Lean/Coq/Agda. That difference shapes everything.

Isabelle's strength — automation

Isabelle has the strongest automation in the field.

- `auto` — the strongest general auto-prover

- `metis` — first-order ATP back-end

- `sledgehammer` — throws the current goal at **external SMT/ATP solvers** (Z3, CVC4, E, Vampire, etc.) and reconstructs the discovered proof inside Isabelle

theorem add_comm: "(a::nat) + b = b + a"

by (induct a) auto

One line. In Lean you would call `simp` or `omega`, or write out the induction longer. Isabelle is "automation first" by philosophy.

Isabelle's flagship achievements

- **The seL4 microkernel** — NICTA (now CSIRO Data61) and UNSW used about 200,000 lines of Isabelle proofs to verify a 9,000-line C microkernel for functional correctness, integrity, and confidentiality. **The most strongly verified operating-system code ever written by humans.**

- **Archive of Formal Proofs (AFP)** — the curated repository of Isabelle proofs. 700+ entries as of 2026.

Isabelle's place in 2026

The tool that goes deepest into industrial verification and OS security. The maths library is smaller than mathlib, but the automation is unmatched. If you are working on seL4, Isabelle is effectively mandatory.

8. F* (FStar, Microsoft) — HACL* crypto verification

F*'s identity

F\* (pronounced "F-star") is Microsoft Research's **dependently-typed, SMT-automated, ML-flavoured** proof-oriented programming language. On the dependent-types side it is in the same lineage as Coq/Lean, but it makes **Z3 a first-class citizen**, automating much of the everyday proof burden.

A short F\* snippet

val sorted_insert: x:int -> l:list int{sorted l}

-> Tot (l':list int{sorted l' /\ Set.equal (set_of (x::l)) (set_of l')})

let rec sorted_insert x = function

| [] -> [x]

| y :: tl -> if x <= y then x :: y :: tl

else y :: sorted_insert x tl

Specifications (`sorted l`, `Set.equal …`) go directly into the type. F\* throws this at Z3 and tries to discharge it automatically; if Z3 cannot, the user adds extra lemmas.

HACL* — verified crypto that ships

F\*'s most famous industrial outcome is **HACL\***, a library that formally verifies standard cryptographic algorithms — Curve25519, Poly1305, ChaCha20, SHA-2, HKDF, AES-GCM — in F\* and extracts to C. This code:

- Ships in **Firefox**'s NSS library (signatures, TLS)

- Ships in the **Linux kernel**'s WireGuard VPN

- Ships in parts of **Windows / Azure** TLS handling

So when you use HTTPS today, F\*-verified code is very likely running somewhere in that connection.

EverCrypt / EverParse / Project Everest

HACL\* lives under the larger umbrella of **Project Everest** — EverCrypt (multi-algorithm dispatch), EverParse (verified message parsers), and more. See [`project-everest.github.io`](https://project-everest.github.io/).

F* vs Lean

| Aspect | F* | Lean 4 |

| --- | --- | --- |

| Automation | Z3 first-class | tactics + SMT separately |

| Extraction | C, OCaml, .NET, JS | C, IR (in progress) |

| Industry | HACL*, Project Everest | mathlib, AWS |

| Maths library | Small | Huge (mathlib) |

9. Liquid Haskell — refinement types

Liquid Haskell's identity

Liquid Haskell, from Ranjit Jhala's group at UCSD, is a **refinement-type system for Haskell**. You do not learn a new language — annotate ordinary Haskell code with refinement specs and an SMT solver (typically Z3) verifies them.

A short example

{-@ type Pos = {v:Int | v > 0} @-}

{-@ divide :: Int -> Pos -> Int @-}

divide :: Int -> Int -> Int

divide x y = x `div` y

{-@ measure size @-}

size :: [a] -> Int

size [] = 0

size (_:xs) = 1 + size xs

{-@ type NonEmpty a = {v:[a] | size v > 0} @-}

{-@ head :: NonEmpty a -> a @-}

head :: [a] -> a

head (x:_) = x

The comments between `{-@` and `@-}` are **refinement specs**. The compiler still sees ordinary Haskell, but the `liquid` tool checks the specs via SMT.

Strengths and weaknesses

- **Strength**: verify Haskell code without learning a dependently-typed language. The entry barrier is low.

- **Weakness**: confined to Haskell. Not usable for general theorem proving. If Z3 cannot solve a spec, you are stuck.

For pragmatic "verified Haskell in industry," Liquid Haskell is the realistic first choice.

10. AI assistance — DeepMind AlphaProof (IMO 2024 silver)

What AlphaProof was

In July 2024, DeepMind announced that **AlphaProof** and **AlphaGeometry 2** had solved 4 of the 6 problems at IMO 2024 (28 of 42 points) — a **silver-medal score**. Each problem took days (human contestants must finish under exam time), but solving four problems including the hardest P6 (combinatorics) was a watershed.

The shape of the system:

1. **Natural-language IMO problem → Lean 4 theorem** via an auto-formaliser

2. **Reinforcement learning inside Lean 4 to search for proofs** (AlphaProof = AlphaZero + Lean)

3. Geometry problems went to **AlphaGeometry 2** (successor to 2023's AlphaGeometry)

DeepMind's [published Lean proofs](https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html) read very inhuman — every line formally checked.

Follow-up in 2025–2026

- Similar (unofficial) IMO 2025 results were reported

- DeepMind continues to pair [AlphaProof with LLMs](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/)

- The Lean 4 coupling keeps deepening

Why it matters

LLMs went from "plausible-sounding prose" to **formally verified solutions**. Correctness is decided by the compiler — hallucination is structurally blocked.

11. Anthropic + AIMO ($5M prize)

AI Mathematical Olympiad (AIMO)

**AIMO** is a $10M AI-mathematics challenge funded by XTX Markets. Of that, the **Grand Prize of $5M** goes to a model that hits a target accuracy on 50 IMO-level problems. (Official site: [aimoprize.com](https://aimoprize.com/).)

Progress Prize rounds during 2024-2025 saw rapid open-source progress — NuminaMath among others. As of 2026 the Grand Prize is (publicly) not yet awarded, but most observers report the gap is closing.

Anthropic joining in

Since late 2024, Anthropic has made **mathematical reasoning and Lean formalisation** an explicit evaluation target for Claude. From Anthropic's published reports:

- Claude generates natural-language solutions and then formalises them in Lean with steadily less human intervention

- A workflow where Claude receives the Lean InfoView as context and proposes one tactic at a time is taking hold in the mathlib community (see [Lean Copilot](https://github.com/lean-dojo/LeanCopilot))

- LLM-assisted PRs to mathlib grew through 2025-2026

LeanDojo / LeanCopilot / ntp

The academic side has the same current:

- **LeanDojo** (CMU) — an RL / tool environment so LLMs can drive Lean

- **LeanCopilot** — in-editor LLM tactic suggestions inside Lean

- **ntp-toolkit** — standardised next-tactic-prediction benchmark

These are merging into "AI-assisted formalisation" as a normal mathlib practice.

12. Terence Tao + Lean — a first-rank mathematician joining

What brought Tao to Lean

Terence Tao (UCLA, Fields Medal 2006) is one of his generation's pre-eminent analysts. Since 2023 he has been posting Lean formalisation results regularly on `terrytao.wordpress.com`.

Headline events:

1. **Nov 2023 — PFR Project** — Tao, Gowers, Green, and Manners' proof of the [Polynomial Freiman-Ruzsa conjecture](https://arxiv.org/abs/2311.05762) was formalised in Lean. About three weeks with 20+ collaborators. Tao cites it as the model "blueprint workflow."

2. **2024 — Magma equation classification** — a systematic classification of 4,694 magma equations in Lean. A showcase of breaking a mathematical problem into a Lean blueprint solved by distributed collaboration.

3. **2025-2026** — Tao starts writing parts of his own new papers in Lean from scratch, publicly using GitHub Copilot / Claude as an assistant.

Tao's message

Across multiple talks (IAS, Joint Mathematics Meetings):

- "Ten years ago formalising one page of a proof took a year. Today it takes a week. Within five years it will be same-day."

- "A verified library is the mathematician's unit test — assurance that the results we cite really hold."

- "AI takes the dullest part of formalisation. The mathematician moves up the stack."

Kevin Buzzard and undergraduate education

Kevin Buzzard (Imperial College) hands first-year undergraduates the browser-based [Natural Number Game](https://adam.math.hhu.de/#/g/leanprover-community/nng4) Lean puzzle and argues publicly that **every undergraduate mathematician should learn Lean**. By 2026 this has become a regular course at 5-10 top universities.

13. Z3 + CVC5 — the SMT engines underneath

What an SMT solver is

An SMT (Satisfiability Modulo Theories) solver is an engine that automatically decides whether a first-order formula is satisfiable. Where a proof assistant is "the human writes the proof one line at a time," an SMT solver is "throw the formula in as a block and get an automatic answer."

Z3

**Z3** comes from Microsoft Research (2007 onward; Leonardo de Moura was lead author) and is the most influential SMT solver. Free, open source (MIT). Industrial uses:

- F\* / Liquid Haskell back-end

- Microsoft Driver Verifier

- AWS Zelkova (S3 policy verification)

- Standard back-end for compiler verifiers, model checkers, static analysers

CVC5

**CVC5** (Stanford and partners; successor to CVC4, 2022 onward) is Z3's strongest rival. In some domains (strings, datatypes) it outruns Z3. In SMT-COMP competitions Z3 and CVC5 trade first and second place every year.

A short SMT-LIB snippet

(set-logic QF_LIA)

(declare-const x Int)

(declare-const y Int)

(assert (> x 0))

(assert (> y 0))

(assert (= (+ x y) 10))

(check-sat)

(get-model)

`QF_LIA` is "quantifier-free linear integer arithmetic." Both solvers accept the same SMT-LIB input.

Their place in 2026

- Back-end for **F\***, **Dafny** (MS), **Why3** (INRIA)

- One of the candidate solvers **Sledgehammer** (Isabelle) throws goals at

- **AWS Zelkova / Tiros** — SMT-based safety checks for IAM policies in real time

- **Java PathFinder, KLEE** — path-constraint solvers for symbolic execution

> SMT solvers are an "engine room" that proof-assistant users seldom think about, but one of these two is humming behind almost every automated step.

14. Formal verification in industry — seL4 / CompCert / IronFleet / KLEE

seL4 — a verified microkernel

[seL4](https://sel4.systems/), announced in 2009 by NICTA (now CSIRO Data61) and UNSW, was the first serious OS kernel verified end-to-end. About **9,000 lines of C** were proved correct with **200,000+ lines of Isabelle/HOL proof**, showing:

- **Functional correctness** — the C code behaves exactly like the abstract spec

- **Integrity** — unauthorised access is impossible

- **Confidentiality** — information-flow constraints are preserved

seL4 ships in military avionics, satellites, and some autonomous-driving systems today. The seL4 Foundation maintains it as open source.

CompCert — a verified C compiler

Xavier Leroy's (INRIA, Collège de France) [CompCert](https://compcert.org/) is **a C compiler written and verified in Coq (now Rocq)**. It takes a near-complete subset of C and compiles to PowerPC / ARM / x86 assembly, proving in Rocq that "source C semantics == output assembly semantics."

CSmith fuzzing found dozens of compiler bugs in GCC and Clang. In CompCert it found **zero compiler bugs** (a few spec-gap issues only). Airbus and similar aerospace shops use it in production.

IronFleet / IronClad

Microsoft Research's [IronFleet](https://www.microsoft.com/en-us/research/project/ironclad/) verified end-to-end distributed systems (Paxos, lock service) in **Dafny** (Z3 back-end). The first real-world demonstration of simultaneously proving safety, liveness, and linearisability in a non-Byzantine setting.

KLEE — symbolic execution

[KLEE](https://klee-se.org/) is a symbolic-execution engine over LLVM IR. Different in kind from full verification (partial path exploration) but extremely effective at finding real bugs in real code. KLEE found large numbers of bugs in coreutils, BusyBox, and others.

Summary table

| Tool | What it verifies | Back-end |

| --- | --- | --- |

| seL4 | OS kernel | Isabelle/HOL |

| CompCert | C compiler | Rocq |

| IronFleet | Distributed systems | Dafny + Z3 |

| HACL* / EverCrypt | Crypto libraries | F* + Z3 |

| KLEE | General LLVM | SMT (Z3/STP) |

| AWS Zelkova | IAM policies | Z3 |

15. Korea / Japan — KAIST, ETRI, Kyoto, Tokyo, AIST

Korea

- **KAIST CS PL/Verification group** — the Software Reliability Lab (SRL, [psl.kaist.ac.kr](https://psl.kaist.ac.kr/)) runs Coq/Rocq-based formal-verification research. Prof. Jeehoon Kang's group is known for CompCert extensions.

- **POSTECH** and **Seoul National University PL labs** keep functional / type-theoretic / verification work going steadily.

- **ETRI Formal Verification group** — government-funded OS/security verification.

- Few universities have made Coq/Lean a regular undergraduate course yet, but adoption rose from 2024-2026.

Japan

- **Kyoto University Kinoshita lab / Igarashi lab** — long-standing PL / type-theory tradition in Japan, Coq-heavy.

- **University of Tokyo Hasuo lab / Kobayashi lab** — formal verification and model checking.

- **AIST Cyber Physical Security Research Center** — Z3 / CVC5 / Isabelle for security verification.

- **NII (National Institute of Informatics)** — mathematical-logic and type-theory research.

- An automata-theory plus theorem-proving community (ALGI and similar) is alive.

Korean / Japanese resources

- Korean: KAIST CS220 course materials by Prof. Kang, scattered blogs (`hyperpolyglot`, Jaesun Kim, etc.). Volume is small.

- Japanese: blogs like `qnighy` (Microsoft, Rust/Coq) and `mzp`. More active than in Korea.

> Both countries effectively default to English resources (mathlib Zulip, Coq Discourse, FStar GitHub) as the standard.

16. Who should learn a proof assistant?

Undergraduate mathematicians

**Lean 4 + mathlib** is the clear first choice. Spend a week with Imperial College's browser-based [Natural Number Game](https://adam.math.hhu.de/#/g/leanprover-community/nng4), then go chapter by chapter through [`Mathematics in Lean`](https://leanprover-community.github.io/mathematics_in_lean/). Within six months you can formalise the theorems of your own undergrad courses.

Graduate mathematicians / researchers

If the goal is **formalising your own papers + contributing to mathlib**, choose Lean. Watch Tao. But if your subfield is already heavily on Coq/Rocq or Isabelle (parts of number theory, parts of topology), follow that current — it is more efficient.

PL researchers / compiler / type-system folk

**Rocq (Coq)** or **Agda**. CompCert, Iris, and the Software Foundations lineage live here. Agda is essential if you care about HoTT / Cubical.

Security engineers / crypto engineers

**F\*** or **Isabelle/HOL**. To work on HACL\* / EverCrypt, learn F\*. For OS / microkernel security, the seL4 → Isabelle path.

Backend / general developers

Start with **Dafny**, **Liquid Haskell**, or **TLA+** (Lamport). Lower entry barrier than full proof assistants, and they apply directly to code and specs.

"Just curious" people

Start with the games at [Lean Game Server](https://adam.math.hhu.de/). Natural Number Game, Set Theory Game, Cantor's World — all run in a browser. An hour and you've completed your first proof.

17. Closing — formalisation is no longer "the future"

The 2026 picture:

1. **Lean 4 + mathlib** is the de-facto standard for mathematics formalisation. One million theorems, a daily tool for top mathematicians.

2. **Rocq (formerly Coq)** holds industrial verification (CompCert, seL4 auxiliaries) and 25 years of history.

3. **Agda / Idris 2** keep their place as the tools of type theory and PL research.

4. **Isabelle/HOL + sledgehammer** makes industrial verification like seL4 possible through depth of automation.

5. **F\* + Z3 + HACL\*** is already inside the HTTPS you use today.

6. **DeepMind AlphaProof and Anthropic AIMO** opened the AI-assisted-formalisation era. Lean and LLMs are routinely pair-programming.

7. **seL4, CompCert, and IronFleet** demolished the excuse that "formal verification is academic." It runs in real systems.

If you said a decade ago that "formalisation will soon become standard," you would have been laughed at. Say the same thing in 2026 and the answer is **it already has**.

To mathematicians: start Lean 4. Tao already did.

To security engineers: your next crypto code should go through F\* verification.

To systems engineers: the era of building components on top of seL4 is arriving.

To everyone curious: spend an hour on the [Lean Game Server](https://adam.math.hhu.de/).

Proof is no longer a thing of paper.

References

- Lean Prover (official) — [lean-lang.org](https://lean-lang.org/)

- Lean Community — [leanprover-community.github.io](https://leanprover-community.github.io/)

- mathlib4 GitHub — [github.com/leanprover-community/mathlib4](https://github.com/leanprover-community/mathlib4)

- Mathematics in Lean — [leanprover-community.github.io/mathematics_in_lean](https://leanprover-community.github.io/mathematics_in_lean/)

- Lean Game Server (Natural Number Game and friends) — [adam.math.hhu.de](https://adam.math.hhu.de/)

- Theorem Proving in Lean 4 — [leanprover.github.io/theorem_proving_in_lean4](https://leanprover.github.io/theorem_proving_in_lean4/)

- Leonardo de Moura, Lean FRO — [lean-fro.org](https://lean-fro.org/)

- Rocq Prover (ex-Coq) — [rocq-prover.org](https://rocq-prover.org/)

- Coq → Rocq renaming announcement (March 2024) — [coq.discourse.group/t/coq-renaming-from-coq-to-rocq/2243](https://coq.discourse.group/t/coq-renaming-from-coq-to-rocq/2243)

- mathcomp / Ssreflect — [math-comp.github.io](https://math-comp.github.io/)

- Software Foundations (Pierce et al., Coq/Rocq) — [softwarefoundations.cis.upenn.edu](https://softwarefoundations.cis.upenn.edu/)

- Agda (official) — [wiki.portal.chalmers.se/agda](https://wiki.portal.chalmers.se/agda/pmwiki.php)

- PLFA (Programming Language Foundations in Agda) — [plfa.github.io](https://plfa.github.io/)

- Idris 2 — [idris-lang.org](https://www.idris-lang.org/)

- Edwin Brady, Type-Driven Development with Idris (Manning)

- Isabelle (official) — [isabelle.in.tum.de](https://isabelle.in.tum.de/)

- Archive of Formal Proofs — [isa-afp.org](https://www.isa-afp.org/)

- F* (FStar) — [fstar-lang.org](https://www.fstar-lang.org/)

- HACL* / EverCrypt / Project Everest — [project-everest.github.io](https://project-everest.github.io/)

- Liquid Haskell — [ucsd-progsys.github.io/liquidhaskell](https://ucsd-progsys.github.io/liquidhaskell/)

- DeepMind AlphaProof IMO 2024 — [deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/)

- AIMO (AI Mathematical Olympiad) — [aimoprize.com](https://aimoprize.com/)

- LeanDojo — [leandojo.org](https://leandojo.org/)

- Lean Copilot — [github.com/lean-dojo/LeanCopilot](https://github.com/lean-dojo/LeanCopilot)

- Terence Tao's blog — [terrytao.wordpress.com](https://terrytao.wordpress.com/)

- PFR Conjecture (Gowers, Green, Manners, Tao, 2023) — [arxiv.org/abs/2311.05762](https://arxiv.org/abs/2311.05762)

- Z3 (official) — [github.com/Z3Prover/z3](https://github.com/Z3Prover/z3)

- CVC5 (official) — [cvc5.github.io](https://cvc5.github.io/)

- SMT-LIB standard — [smt-lib.org](https://smt-lib.org/)

- seL4 Foundation — [sel4.systems](https://sel4.systems/)

- CompCert (Xavier Leroy, INRIA) — [compcert.org](https://compcert.org/)

- IronFleet / Ironclad (Microsoft) — [microsoft.com/en-us/research/project/ironclad](https://www.microsoft.com/en-us/research/project/ironclad/)

- Dafny (official) — [dafny.org](https://dafny.org/)

- KLEE Symbolic Execution Engine — [klee-se.org](https://klee-se.org/)

- TLA+ (Leslie Lamport) — [lamport.azurewebsites.net/tla/tla.html](https://lamport.azurewebsites.net/tla/tla.html)

- AWS Automated Reasoning — [aws.amazon.com/security/provable-security](https://aws.amazon.com/security/provable-security/)

- AWS Zelkova (IAM policy verification, Z3) — Provable Security blog

- KAIST PSL — [psl.kaist.ac.kr](https://psl.kaist.ac.kr/)

- ETRI formal-verification group — [etri.re.kr](https://www.etri.re.kr/)

- Kyoto University Igarashi lab — [fos.kuis.kyoto-u.ac.jp](https://www.fos.kuis.kyoto-u.ac.jp/)

- AIST Cyber Physical Security — [aist.go.jp](https://www.aist.go.jp/)

- Kevin Buzzard's Xena project blog — [xenaproject.wordpress.com](https://xenaproject.wordpress.com/)

- ITP (Interactive Theorem Proving) conference — [itp-conference.org](https://itp-conference.github.io/)

- CICM (Conferences on Intelligent Computer Mathematics) — [cicm-conference.org](https://cicm-conference.org/)