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

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

1장 · 2026년 정리 증명기 지도 — 6개 진영의 풍경

2026년, 정리 증명기(proof assistant, theorem prover) 생태계는 그 어느 때보다 활기차다. 10년 전 "수학자들의 장난감"이라 불리던 도구들이, 지금은 **세계 최고 수학자들의 일상 노트북**이자 **OS 커널과 암호 라이브러리의 안전성 보증서**가 되었다.

지금 이 순간 살아있는 주요 진영은 다음과 같다.

| 진영 | 핵심 | 만든 사람 | 색깔 |

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

여기에 더해 두 가지 흐름이 2026년의 공기를 바꾸고 있다.

1. **AI 보조** — DeepMind AlphaProof가 IMO 2024에서 은메달 점수(7문제 중 4문제, 28/42점)를 받았고, Anthropic은 AI Mathematical Olympiad($5M 상금)와 mathlib 검색·자동 증명에 참여했다. Claude·GPT 계열 LLM은 Lean tactic 생성기로 일상적으로 쓰인다.

2. **현역 일류 수학자의 합류** — Terence Tao(필즈상 2006)는 자기 논문(예: PFR conjecture)을 Lean으로 형식화하는 프로젝트를 공개적으로 진행 중이고, Kevin Buzzard(Imperial College)는 "수학과 학부생이 Lean을 배워야 한다"고 공개 강연한다.

이 글은 위 7개 진영을 한 장씩, 그 다음 AI·SMT·산업 사례를 차례로 짚는다.

> **용어**: proof assistant = "수학자가 증명을 쓰고 컴퓨터가 한 줄씩 검증하는" 도구. SMT solver = "수식이 참인지 자동으로 푸는" 백엔드 엔진(Z3, CVC5). 둘이 합쳐지면 F\*나 Liquid Haskell처럼 일반 코드도 검증할 수 있다.

2장 · Lean 4 — Leonardo de Moura, AWS, 폭발 성장

Lean의 짧은 역사

Lean은 Microsoft Research에서 **Leonardo de Moura**(Z3의 그 사람)가 2013년에 시작한 프로젝트다. Lean 2(2015), Lean 3(2017)을 거쳐 Lean 4가 2021년에 안정화되었다. 2023년 de Moura는 Microsoft를 떠나 **Amazon Web Services**의 Automated Reasoning Group에 합류했다. AWS는 Lean 4 컴파일러 개발과 mathlib 인프라를 후원한다.

Lean 4의 정체성

Lean 4는 단순한 정리 증명기가 아니라 **완전한 의존타입 함수형 프로그래밍 언어**다.

-- 자연수 덧셈의 가환성

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`은 명제, `:=`는 증명이다. `by ... ` 블록 안에서 `induction`, `simp`, `rw`(rewrite) 같은 tactic을 호출해 한 단계씩 목표를 해결한다.

Lean 4가 빠른 이유

- **자체 컴파일러**: Lean 4 자체가 Lean으로 작성되었다(self-hosting). C로 컴파일되어 native 성능을 낸다.

- **매크로 시스템**: Racket 스타일의 매크로로 도메인 특화 문법을 사용자가 만들 수 있다. mathlib는 이를 사용해 수학 표기를 그대로 쓴다.

- **타입 클래스**: Haskell 스타일 타입 클래스로 추상화가 깔끔하다.

설치와 첫 증명

elan: Lean 버전 매니저 (rustup 같은 것)

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

새 프로젝트

lake new my_first_lean

cd my_first_lean

lake build

VS Code에 Lean 4 익스텐션을 설치하면 마우스 hover로 현재 goal과 타입을 실시간으로 본다. 이 InfoView가 Lean 사용자가 사랑하는 첫 번째 이유다.

2026년 현재 상태

- Lean 4.10+ 안정

- mathlib는 100만 개 정리 돌파 (다음 장)

- 학부 강의 채택: Imperial College, Brown, Berkeley, CMU

- 산업: AWS Automated Reasoning, Galois, Kestrel Institute

> Lean Community 사이트 [leanprover-community.github.io](https://leanprover-community.github.io/)와 [Zulip 채팅](https://leanprover.zulipchat.com/)은 사실상 24/7 살아있다. 질문을 올리면 보통 한 시간 안에 누군가 답한다.

3장 · mathlib — 100만 정리, Terence Tao의 노트북

mathlib란 무엇인가

**mathlib4**(Lean 4용)는 인류 역사상 가장 큰 형식화된 수학 라이브러리다. 2026년 5월 현재:

- **1,000,000+ 정리** (theorem/lemma/def 합산, 2026년 초 돌파)

- **약 30만 줄의 정의, 80만 줄의 증명**

- 600+ 명의 기여자 (`git log`)

- 그룹, 환, 체, 위상, 측도, 범주, 해석, 대수기하…거의 모든 학부+대학원 수학

구조와 표기

-- 실해석학: 적분의 단조성

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

이렇게 일반 수학과 거의 같은 표기를 쓰는 것이 mathlib의 핵심이다. `ℝ`, `∫`, `≤`는 그냥 유니코드 글자다. Lean 4의 매크로 시스템이 이걸 가능하게 한다.

Terence Tao와 PFR Project

2023년 11월, Terence Tao(필즈상)는 Tim Gowers, Ben Green, Freddie Manners와 함께 증명한 [Polynomial Freiman-Ruzsa 추측](https://arxiv.org/abs/2311.05762) 정리를 **3주 만에** Lean으로 형식화하는 프로젝트를 시작했다. 결과는 그가 자기 블로그(`terrytao.wordpress.com`)에 공개적으로 기록했다.

핵심 메시지: **"이제 수학자가 형식화에 한 달도 안 걸리고, AI 보조가 점점 더 많이 한다."**

2026년 현재 Tao는 자기의 새 논문들 일부를 처음부터 Lean으로 작성하기 시작했다.

누가 mathlib에 기여하는가

- Imperial College (Kevin Buzzard 그룹)

- Brown University (Heather Macbeth)

- 카네기멜런 (Jeremy Avigad)

- 다수의 PhD 학생, 학부생, 취미 수학자

- 점차 AI 보조 (다음 장에서)

첫 PR 가이드

mathlib는 진입장벽이 낮다. 처음 기여하는 사람을 위한 가이드와 [contribute 페이지](https://leanprover-community.github.io/contribute/index.html)가 있다. 정리 하나, 정의 하나, 보조 보조정리 하나도 환영이다.

4장 · Rocq (구 Coq, 2024.3 리브랜드) — 25년의 클래식

왜 이름이 바뀌었나

2024년 3월, Coq 개발팀은 [공식 발표](https://coq.discourse.group/t/coq-renaming-from-coq-to-rocq/2243)로 **Coq를 Rocq로 리브랜드**한다고 밝혔다. 이유는 두 가지로 요약된다.

1. "Coq"라는 단어가 일부 언어에서 외설적인 의미로 들려 신규 사용자 진입에 장벽이 됨

2. 새 세대의 정체성 — Lean이 사용자를 끌어가는 와중에 Rocq 자신을 재정의할 시점

이름은 `coq.inria.fr` 도메인을 거쳐 [`rocq-prover.org`](https://rocq-prover.org/)로 옮겨갔다. 코드 베이스 자체는 그대로 25년 역사를 이어간다(Coq 1.0이 1989년).

Rocq의 강점

- **튼튼한 산업 검증 기록** — CompCert(아래), seL4 보조, Verdi(분산시스템), CertiCrypt, Iris 등

- **Coq Standard Library**가 매우 안정적

- **Ssreflect / mathcomp** — Gonthier가 4색 정리, Feit–Thompson 정리(255쪽)를 증명할 때 만든 strategy 라이브러리. Lean의 mathlib보다 오래되었다.

- **OCaml 기반** — INRIA의 OCaml 생태계와 단단히 연결됨

짧은 Rocq 예시

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`. Lean과 모양은 비슷하지만 문법이 더 LISP스럽다(`Qed.`로 닫기).

2026년 Rocq vs Lean

| 항목 | Rocq | Lean 4 |

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

| 역사 | 1989~ | 2013~ |

| 라이브러리 | mathcomp, stdlib | mathlib (1M+) |

| 신규 채택 | 정체 / 감소 | 폭발 성장 |

| 산업 | CompCert, ProofGeneral | AWS Automated Reasoning |

| 입문 난이도 | 가파름 | 가파르지만 Lean Game이 있음 |

Rocq가 죽었다는 뜻은 아니다 — 25년 누적된 산업 코드베이스는 어디 가지 않고, INRIA와 다수 학교가 여전히 강력히 지원한다.

5장 · Agda — 의존적 타입의 표본

Agda의 자리

Agda는 스웨덴 Chalmers 공과대학에서 시작된 **순수 의존타입 함수형 언어**다. Lean과 달리 "프로그래밍 언어로서의 정체성"이 더 강하다 — 즉 모든 함수는 종료해야 하고(totality check), 타입과 값의 구분이 거의 없다.

Agda의 표기 — 유니코드 천국

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))

`ℕ`, `≡`, `∀`, `→` 모두 유니코드. 입력은 Emacs/VS Code의 Agda 모드가 `\to`, `\equiv`, `\forall`을 변환해 준다.

Agda의 강점

- **타입과 값이 완전히 동일** — Lean보다 한 단계 더 순수

- **Cubical Agda** — Homotopy Type Theory의 표준 구현

- **PLFA**([Programming Language Foundations in Agda](https://plfa.github.io/)) — 학습 자료의 최고봉

Agda의 약점

- 큰 표준 라이브러리가 없음(`agda/stdlib`이 있지만 mathlib에 비할 바 못 됨)

- 산업 채택 거의 없음

- 자동화(tactic)가 매우 약함 — 거의 수동 증명

2026년에 Agda를 배워야 하나

목적이 **타입 이론 학습**, **HoTT 연구**, **PL 연구**라면 그렇다. 산업 검증이나 큰 수학 라이브러리가 목적이라면 Lean 4가 낫다.

6장 · Idris 2 — Edwin Brady의 실용 의존타입

Idris 2의 정체성

Idris는 영국 St Andrews의 **Edwin Brady**가 만든 의존타입 함수형 언어다. Idris 1(2011)이 Haskell로 작성된 학술 프로토타입이었다면, **Idris 2**(2020~)는 Idris 자체로 다시 작성한 self-hosting 버전이고, 결정적으로 **Quantitative Type Theory**(QTT, Bob Atkey)를 채택했다.

Idris 2의 핵심 — 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

-- 컴파일 타임에만 존재하는 인덱스 (0 quantity)

data Vect : Nat -> Type -> Type where

Nil : Vect 0 a

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

QTT는 각 인자에 **0 / 1 / many** 수량을 부여한다. `0`은 컴파일 타임에만, `1`은 정확히 한 번, `many`는 평범한 변수. 이걸로 의존타입과 선형타입을 동시에 다룬다.

Idris 2가 노리는 자리

Idris는 "프로그래밍을 위한 의존타입"을 가장 직설적으로 노린다. Lean이 수학, Agda가 PL 이론에 가까운 반면, Idris는 **실제 소프트웨어 개발**을 의식한다.

- 단점: 커뮤니티가 작다, 라이브러리가 적다

- 장점: Brady의 책 [*Type-Driven Development with Idris*](https://www.manning.com/books/type-driven-development-with-idris)는 의존타입 입문서의 표준

7장 · Isabelle/HOL — seL4를 증명한 도구

Isabelle의 정체성

Isabelle은 영국 Cambridge의 Larry Paulson과 독일 TUM의 Tobias Nipkow가 1986년부터 개발해온 **고전 HOL(High-Order Logic) 기반** 증명 보조기다. Lean/Coq/Agda가 **constructive logic + 의존타입**을 쓰는 반면, Isabelle/HOL은 **고전 논리 + 단순타입**을 쓴다.

Isabelle의 강점 — 자동화

Isabelle은 자동화가 매우 강력하다.

- `auto` — 가장 강한 일반 자동 증명

- `metis` — first-order ATP backend

- `sledgehammer` — **외부 SMT/ATP**(Z3, CVC4, E, Vampire 등)에 목표를 던지고 그들이 찾은 증명을 Isabelle 안에서 재구성

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

by (induct a) auto

한 줄. Lean이라면 `simp`나 `omega`를 호출하거나, 더 길게 induction을 풀어 쓴다. Isabelle은 "자동화 우선" 철학이다.

Isabelle의 대표 업적

- **seL4 마이크로커널** — NICTA(현 CSIRO Data61)와 UNSW가 약 200,000 LoC의 Isabelle 증명으로 9,000 LoC의 C 커널의 기능적 정확성, 무결성, 비밀성을 증명. **사람이 작성한 OS 코드 중 가장 강하게 검증된** 코드.

- **Archive of Formal Proofs (AFP)** — Isabelle 증명의 큐레이트된 저장소. 2026년 기준 700+ 항목.

2026년 Isabelle의 자리

산업 검증과 OS 보안에 가장 깊이 들어가 있는 도구. mathlib같은 수학 라이브러리는 적지만 자동화의 깊이는 압도적이다. seL4를 만진다면 사실상 Isabelle이 강제된다.

8장 · F* (FStar, Microsoft) — HACL* 암호 검증

F*의 정체성

F\*(영어로 "FStar")는 Microsoft Research가 만든 **의존타입 + SMT 자동화 + ML계 문법**의 증명 지향 프로그래밍 언어다. 의존타입 측면에서는 Coq/Lean과 같은 계통이지만, **Z3 SMT 솔버를 첫 번째 시민**으로 가져와 일상적인 증명 책임의 상당 부분을 자동화한다.

짧은 F\* 예시

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

타입 안에 직접 사양(`sorted l`, `Set.equal …`)을 박는다. F\*는 이걸 Z3에 던져 자동으로 풀려고 시도하고, 풀리지 않으면 사용자가 보조정리를 보강한다.

HACL* — 실제로 들어간 검증된 암호

F\*의 가장 유명한 산업 사례는 **HACL\*** — Curve25519, Poly1305, ChaCha20, SHA-2, HKDF, AES-GCM 등 표준 암호 알고리즘을 F\*로 검증하고 C로 추출(extract)한 라이브러리다. 이 코드는:

- **Firefox**의 NSS 라이브러리(서명, TLS)에 들어감

- **Linux 커널**의 WireGuard VPN에 들어감

- **Windows / Azure**의 일부 TLS 처리에 사용됨

즉 당신이 오늘 HTTPS를 쓸 때, F\*로 검증된 코드가 그 어딘가에서 돌고 있을 가능성이 매우 높다.

EverCrypt / EverParse / Project Everest

HACL\*는 더 큰 우산인 **Project Everest** 아래에 있다. EverCrypt(다중 알고리즘 디스패치), EverParse(검증된 메시지 파서) 등이 함께 묶여 있다. [`project-everest.github.io`](https://project-everest.github.io/)에 정리되어 있다.

F* vs Lean

| 항목 | F* | Lean 4 |

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

| 자동화 | Z3 첫 번째 시민 | tactic + SMT는 별도 |

| 추출 | C, OCaml, .NET, JS | C, IR (작업 중) |

| 산업 | HACL*, Project Everest | mathlib, AWS |

| 수학 라이브러리 | 적음 | 거대(mathlib) |

9장 · Liquid Haskell — refinement types

Liquid Haskell의 정체성

Liquid Haskell은 UCSD의 **Ranjit Jhala** 그룹이 만든 **Haskell용 refinement type 시스템**이다. 새로운 언어를 배우지 않고, 평범한 Haskell 코드에 사양 주석을 달면 SMT 솔버(주로 Z3)가 검증한다.

짧은 예시

{-@ 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

`{-@ ... @-}` 안의 주석이 **refinement spec**이다. 컴파일러는 평범한 Haskell이지만, `liquid` 도구가 SMT로 사양을 검증한다.

강점과 약점

- **강점**: 의존타입 언어를 배우지 않고도 Haskell 코드를 검증할 수 있다. 진입장벽이 낮다.

- **약점**: Haskell 안에 갇혀 있다. 일반 정리 증명에는 못 쓴다. Z3에 못 풀리는 사양은 거기서 막힌다.

진짜 "산업의 검증된 Haskell"을 노린다면 Liquid Haskell이 현실적 첫 선택이다.

10장 · AI 보조 — DeepMind AlphaProof (IMO 2024 은메달)

AlphaProof란 무엇이었나

2024년 7월, DeepMind는 **AlphaProof**와 **AlphaGeometry 2**가 IMO 2024(국제수학올림피아드) 6문제 중 4문제(28/42점)를 풀어 **은메달 점수**를 받았다고 발표했다. 4문제 모두 정답에 도달하는 데 며칠씩 걸렸지만(인간 참가자는 시험 시간 안에 풀어야 함), 가장 어려운 P6(combinatorics)를 포함해 4개를 정답으로 풀어낸 것은 큰 사건이었다.

핵심 구조:

1. **자연어 IMO 문제 → Lean 4 정리**로 자동 번역 (auto-formalizer)

2. **Lean 4 안에서 강화학습으로 증명 탐색**(AlphaProof = AlphaZero + Lean)

3. 기하 문제는 **AlphaGeometry 2**(2023년 AlphaGeometry의 후속)가 따로 처리

DeepMind가 공개한 [Lean 증명 자체](https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html)는 사람이 봐도 매우 비인간적이다 — 100% 형식화된 한 줄 한 줄.

2025~2026년 후속

- 2025년 IMO에서도 비공식적으로 비슷한 성과를 냈음(여러 비공식 보고)

- DeepMind는 [AlphaProof + LLM 페어](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/) 작업을 계속함

- Lean 4와의 결합이 점점 깊어짐

의의

LLM이 자연어 풀이를 적당히 생성하던 시절을 지나, **형식적으로 검증된 풀이**를 생성하는 시대로 들어갔다. 정답 여부를 컴파일러가 즉시 판정해 준다 — hallucination이 원리적으로 차단된다.

11장 · Anthropic + AIMO ($5M 상금)

AI Mathematical Olympiad (AIMO)

**AIMO**는 XTX Markets가 후원하는 \$10M 규모의 AI 수학 올림피아드 챌린지다. 그 중 **Grand Prize \$5M**은 IMO 수준의 문제 50개 중 일정 정확도 이상을 달성하는 AI 모델에 주어진다. (참고: AIMO 공식 사이트 [aimoprize.com](https://aimoprize.com/))

2024~2025년에 진행된 Progress Prize 라운드들에서 NuminaMath 등 여러 오픈소스 모델이 빠르게 발전했다. 2026년 현재 Grand Prize는 아직 수여되지 않았지만(공개적으로), 격차가 줄어들고 있다는 관측이 다수다.

Anthropic의 합류

Anthropic은 2024년 후반부터 **수학 추론과 Lean 형식화**를 Claude 모델의 명시적 평가 항목에 포함시켰다. 공개된 [Claude의 수학 능력 기술 보고](https://www.anthropic.com/news)들에 따르면:

- Claude는 자연어 수학 풀이를 생성하고, Lean으로 형식화할 때 점점 더 적은 사람 개입으로 끝낸다

- Lean InfoView를 Claude가 컨텍스트로 받아 한 단계씩 tactic을 제안하는 워크플로가 mathlib 커뮤니티에 점점 자리잡고 있다 (예: [Lean Copilot](https://github.com/lean-dojo/LeanCopilot) 프로젝트)

- mathlib에 LLM 보조로 작성된 PR이 2025~2026년에 늘어났다

LeanDojo / LeanCopilot / ntp

학계에서도 비슷한 흐름이 있다.

- **LeanDojo** (CMU) — Lean 환경을 LLM이 다룰 수 있게 만든 RL/툴 환경

- **LeanCopilot** — Lean 안에서 직접 LLM tactic 제안

- **ntp-toolkit** — Next-tactic prediction 표준 평가

이 도구들이 점점 합쳐져 "AI 보조 형식화"가 mathlib 일상이 되었다.

12장 · Terence Tao + Lean — 일류 수학자의 합류

Tao가 Lean을 만지기 시작한 계기

Terence Tao(UCLA, 필즈상 2006)는 한 세대 최고의 분석학자다. 그는 2023년부터 자기 블로그 `terrytao.wordpress.com`에서 Lean으로 형식화한 결과들을 정기적으로 공유한다.

대표 사건:

1. **2023.11 — PFR Project** — Tim Gowers, Ben Green, Freddie Manners와 공동 증명한 [Polynomial Freiman-Ruzsa conjecture](https://arxiv.org/abs/2311.05762)를 Lean으로 형식화. 약 3주에 20+명의 협업자가 완성. Tao는 이걸 "blueprint workflow"의 모범으로 제시.

2. **2024 — Magma 추측 분류 프로젝트** — 4,694개의 magma equation을 Lean으로 계통적으로 분류. 수학적 문제를 Lean blueprint로 잘게 쪼개 분산 협업으로 해결한 사례.

3. **2025~2026** — Tao는 자기의 새 논문 일부를 처음부터 Lean으로 작성, GitHub Copilot/Claude 보조 받음을 공개.

Tao가 강조하는 변화

Tao 본인이 여러 강연(예: IAS, Joint Mathematics Meetings)에서 강조한 메시지:

- "10년 전 형식화는 1쪽 증명에 1년이 걸렸다. 지금은 1주일이고, 5년 안에 같은 날에 끝난다."

- "검증된 라이브러리는 수학자의 단위 테스트다. 우리가 쓰는 결과가 진짜 옳다는 보증."

- "AI는 형식화의 가장 지루한 부분을 가져간다. 수학자는 더 위로 올라간다."

Kevin Buzzard와 학부 교육

Imperial College London의 Kevin Buzzard는 학부 1학년에게 [Natural Number Game](https://adam.math.hhu.de/#/g/leanprover-community/nng4)이라는 브라우저 Lean 퍼즐을 시키며, "**모든 수학과 학부생은 Lean을 배워야 한다**"고 공개 주장한다. 이 흐름이 2026년에는 5~10개 일류 대학에서 학부 정규 과목으로 자리잡았다.

13장 · Z3 + CVC5 — 그 밑단의 SMT 솔버

SMT solver란

SMT(Satisfiability Modulo Theories) 솔버는 "이 1차 논리식이 어떤 모델에서 참이 되는지" 자동으로 푸는 엔진이다. 정리 증명기가 "사람이 한 줄씩 쓰는" 도구라면, SMT 솔버는 "수식 한 덩어리를 통째로 던지면 자동으로 답하는" 도구다.

Z3

**Z3**는 Microsoft Research(2007~, Leonardo de Moura가 핵심 저자)가 만든 가장 영향력 있는 SMT 솔버다. 무료/오픈소스(MIT). 대표 사례:

- F\* / Liquid Haskell의 백엔드

- Microsoft Driver Verifier

- AWS Zelkova (S3 정책 검증)

- 컴파일러 검증, 모델 체커, 정적 분석기의 표준 백엔드

CVC5

**CVC5**(Stanford + 다수 기관, CVC4의 후속, 2022~)는 Z3의 가장 강한 경쟁자다. 일부 도메인(특히 string, datatype)에서 Z3보다 빠르다. CASC/SMT-COMP 같은 대회에서 Z3와 CVC5가 1, 2위를 다툰다.

짧은 예시 — SMT-LIB

(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`는 "quantifier-free linear integer arithmetic". 두 솔버 모두 같은 표준 입력을 받는다.

2026년의 자리

- **F\***, **Dafny**(MS), **Why3**(INRIA) 등 검증 언어 백엔드

- **Sledgehammer**(Isabelle)가 외부로 던지는 솔버 후보 중 하나

- **AWS Zelkova / Tiros** — IAM 정책의 안전성을 SMT로 검증해 실시간 경고

- **Java PathFinder, KLEE** — 심볼릭 실행에서 path constraint solver

> SMT 솔버는 정리 증명기 사용자가 자주 의식하지 않는 "엔진룸"이지만, 거의 모든 자동화의 뒤에 둘 중 하나가 돌고 있다.

14장 · 형식 검증 사례 — seL4 / CompCert / IronFleet / KLEE

seL4 — 검증된 마이크로커널

2009년 NICTA(현 CSIRO Data61)와 UNSW가 발표한 [seL4](https://sel4.systems/)는 약 **9,000 LoC의 C 마이크로커널**을, **200,000+ LoC의 Isabelle/HOL 증명**으로 검증한 사상 최초의 본격 OS 커널이다. 증명 내용:

- **기능적 정확성** — C 코드가 abstract spec과 행동이 정확히 같다

- **무결성** — 권한 없는 접근이 불가능하다

- **비밀성** — 정보 흐름 제약이 보존된다

이 커널은 군용 항공, 위성, 일부 자율주행 시스템에서 실제로 돌고 있다. seL4 Foundation이 오픈소스로 유지한다.

CompCert — 검증된 C 컴파일러

Xavier Leroy(INRIA, 콜레주 드 프랑스)의 [CompCert](https://compcert.org/)는 **Coq(현 Rocq)로 작성·검증된 C 컴파일러**다. C 표준의 부분집합(거의 전체)을 받아 PowerPC/ARM/x86 어셈블리로 컴파일하면서, "원본 C 의미 == 출력 어셈블리 의미"를 Rocq로 증명한다.

CSmith fuzzing 연구가 GCC/Clang에서는 수십 개의 컴파일러 버그를 찾아낸 반면, CompCert에서는 **단 하나의 컴파일러 버그도 찾지 못했다**(다만 spec gap 일부 발견). Airbus 등 항공 산업에서 실제 사용된다.

IronFleet / IronClad

Microsoft Research의 [IronFleet](https://www.microsoft.com/en-us/research/project/ironclad/)는 분산시스템(Paxos, lock service)을 **Dafny**(Z3 백엔드)로 종단 검증했다. 비잔틴이 아닌 환경에서 안전성/활성성/선형화 가능성을 동시에 증명한 첫 본격 사례.

KLEE — 심볼릭 실행

[KLEE](https://klee-se.org/)는 LLVM IR 위에서 동작하는 심볼릭 실행 엔진이다. 검증과는 결이 다르지만(부분 경로 탐색) 실제 코드의 버그 발견에 매우 효과적이다. coreutils, BusyBox 등에서 수많은 버그를 발견했다.

정리하면

| 도구 | 검증 대상 | 백엔드 |

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

| seL4 | OS 커널 | Isabelle/HOL |

| CompCert | C 컴파일러 | Rocq |

| IronFleet | 분산 시스템 | Dafny + Z3 |

| HACL* / EverCrypt | 암호 라이브러리 | F* + Z3 |

| KLEE | 일반 LLVM | SMT (Z3/STP) |

| AWS Zelkova | IAM 정책 | Z3 |

15장 · 한국 / 일본 — KAIST · ETRI · 京都大学 · 東京大学 · AIST

한국

- **KAIST 전산학부 PL/Verification 그룹** — Software Reliability Lab(SRL, [psl.kaist.ac.kr](https://psl.kaist.ac.kr/)) 등에서 Coq/Rocq 기반 형식 검증 연구. 곽재두 교수 그룹은 CompCert 확장 작업으로 알려짐.

- **POSTECH**, **서울대 PL 연구실** — 함수형/타입 이론/검증 연구가 꾸준함.

- **ETRI 형식 검증 그룹** — 정부 과제로 OS/보안 검증 연구.

- 학부 강의로 Coq/Lean을 정규 도입한 사례는 아직 적지만 2024~2026년 사이 늘고 있다.

일본

- **京都大学木下研究室 / 五十嵐研究室** — PL/타입 이론에서 일본 전통 강자. Coq 활용.

- **東京大学蓮尾研 / 小林研** — formal verification, 모델 체킹.

- **AIST(産業技術総合研究所) Cyber Physical Security Research Center** — Z3/CVC5/Isabelle 활용 보안 검증.

- **NII(国立情報学研究所)** — 수리논리/타입 이론 연구.

- **オートマトン理論**과 정리 증명을 묶는 ALGI 같은 학회 흐름이 살아있다.

한국어 / 일본어 자료

- 한국어: 한경수 교수의 KAIST CS220 자료, 일부 블로그(`hyperpolyglot`, 김재선 블로그 등). 절대량은 적다.

- 일본어: `qnighy`(Microsoft, Rust/Coq), `mzp` 등 일본 Coq/Lean 사용자 블로그. 한국보다 활성화되어 있다.

> 두 나라 모두 영어 자료(mathlib zulip, Coq Discourse, FStar GitHub)로 진입하는 것이 사실상 표준이다.

16장 · 누가 정리 증명기를 배워야 하나

학부 수학생

**Lean 4 + mathlib**이 단연 1순위다. Imperial College의 [Natural Number Game](https://adam.math.hhu.de/#/g/leanprover-community/nng4) (브라우저에서 바로 플레이 가능)을 1주일 해보고, [`Mathematics in Lean`](https://leanprover-community.github.io/mathematics_in_lean/)을 한 챕터씩 따라가면 6개월 안에 자기 학부 과목의 정리들을 형식화할 수 있다.

대학원 수학자 / 연구자

목표가 **자기 논문 형식화 + mathlib 기여**라면 Lean. Tao를 보라. 단, 자기 분야가 이미 Coq/Rocq나 Isabelle에 두텁게 있다면(예: 정수론 일부, 위상 일부) 그 흐름을 따르는 것이 효율적.

PL 연구자 / 컴파일러 / 타입 시스템

**Rocq (Coq)** 또는 **Agda**. CompCert, Iris, software foundations의 흐름이 여기에 있다. Agda는 HoTT/Cubical에 관심 있다면 필수.

보안 엔지니어 / 암호 엔지니어

**F\*** 또는 **Isabelle/HOL**. HACL\*/EverCrypt에 들어가고 싶다면 F\*. OS/마이크로커널 보안이라면 seL4 → Isabelle 경로.

백엔드 / 일반 개발자

**Dafny**, **Liquid Haskell**, 또는 **TLA+**(Lamport)로 시작. 본격 정리 증명기보다 entry barrier가 낮고, 코드/스펙에 바로 적용된다.

"그냥 궁금해서"인 사람

[Lean Game Server](https://adam.math.hhu.de/)의 게임들로 시작하라. Natural Number Game, Set Theory Game, Cantor's World 등이 브라우저에서 돈다. 한 시간이면 첫 증명을 깬다.

17장 · 마무리 — 형식화는 더 이상 미래의 일이 아니다

2026년의 풍경을 정리하면:

1. **Lean 4 + mathlib**가 수학 형식화의 사실상 표준이 되었다. 100만 정리, 일류 수학자의 일상 도구.

2. **Rocq (구 Coq)**는 산업 검증(CompCert, seL4 보조)을 굳건히 유지하며 25년 역사를 잇는다.

3. **Agda / Idris 2**는 타입 이론·PL 연구의 도구로 자리를 지킨다.

4. **Isabelle/HOL + sledgehammer**는 자동화의 깊이로 seL4 같은 산업 검증을 가능케 한다.

5. **F\* + Z3 + HACL\***는 당신이 오늘 쓰는 HTTPS 안에 이미 있다.

6. **DeepMind AlphaProof, Anthropic AIMO**가 AI 보조 형식화 시대를 열었다. Lean과 LLM이 일상적으로 페어 프로그래밍한다.

7. **seL4, CompCert, IronFleet**가 "형식 검증은 학계 이야기"라는 변명을 박살냈다. 실제 시스템에서 돌아간다.

10년 전 "곧 형식화가 표준이 될 것"이라 말했다면 비웃음을 샀을 것이다. 2026년에 같은 말을 하면 **이미 그렇게 되어 있다**고 답해야 한다.

수학자에게: Lean 4를 시작하라. Tao가 이미 했다.

보안 엔지니어에게: 당신의 다음 암호 코드는 F\* 검증을 거쳐야 한다.

시스템 엔지니어에게: seL4 위에서 컴포넌트를 짜는 시대가 곧 온다.

호기심 있는 모두에게: [Lean Game Server](https://adam.math.hhu.de/)를 한 시간만 해보라.

증명은 더 이상 종이 위의 일이 아니다.

참고 / References

- Lean Prover 공식 — [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 등) — [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](https://lean-fro.org/)

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

- Coq → Rocq 리네이밍 발표(2024.3) — [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 공식 — [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 공식 — [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 블로그 — [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 공식 — [github.com/Z3Prover/z3](https://github.com/Z3Prover/z3)

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

- SMT-LIB 표준 — [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 공식 — [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 정책 검증, Z3) — Provable Security 블로그

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

- ETRI 형식 검증 그룹 — [etri.re.kr](https://www.etri.re.kr/)

- 京都大学五十嵐研究室 — [fos.kuis.kyoto-u.ac.jp](https://www.fos.kuis.kyoto-u.ac.jp/)

- AIST 사이버 피지컬 보안 — [aist.go.jp](https://www.aist.go.jp/)

- Kevin Buzzard 블로그 — [xenaproject.wordpress.com](https://xenaproject.wordpress.com/)

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

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