Lean 4 とは何か ── AI が数学オリンピックに挑み、フェルマーの最終定理がコードに書き写される時代の主役言語

はじめに

2024年夏、AI が国際数学オリンピック（IMO）の問題を解き、銀メダル相当の成績を収めました。Google DeepMind の AlphaProof です。

このニュースで見落とされがちな事実が一つあります ── AlphaProof が答案を書いた言語は、英語でも中国語でもなく、Lean 4（リーン・フォー）というプログラミング言語だった、ということです。

同じころ、数学の側でも静かな革命が進んでいます。鍵になる言葉を一つだけ先に説明させてください。形式化（けいしきか）とは、人間の言葉と数式で書かれた数学の証明を、機械が一行ずつ検査できるプログラミング言語のコードへ翻訳して書き写すことです。

数学の世界ではいま、この形式化が最前線の研究者の仕事道具になりつつあります
── フィールズ賞受賞者のテレンス・タオは自らの最新の研究成果をいち早く Lean 4 で形式化 し、英国では「フェルマーの最終定理の証明を丸ごと形式化する」という数年がかりのプロジェクトが始動しました。

人類の数学の到達点を、機械に検査される形へ書き写していく ── その共通の舞台が Lean 4 なのです。

そして2026年春には、日本からも大きなニュースが届きました。

京都大学数理解析研究所の望月新一教授による宇宙際タイヒミュラー理論（IUT 理論）
── 発表から１０年以上、正否をめぐって世界の数学者の意見が分かれ続けてきた巨大理論
── を、Lean 4 の形式化によって中立の立場から検証 する国際プロジェクト LANA が、ZEN 大学の ZEN 数学センターから発表されたのです。

率いるのは加藤文元教授、メンバーには後述するリキッド・テンソル実験を主導した形式化の第一人者たちが名を連ねます。

人間どうしの議論では決着しなかった長年の論争に、機械検査という新しい審判を立てる
── その審判台に選ばれたのも、やはり Lean 4 でした。

• Lean 4 とは何者なのでしょうか？

• 数学者とAI 研究者たちはなぜ、こぞって この言のもとに集うのでしょうか？

• そして、数学者でも AI 研究者でもない普通のソフトウェアエンジニアにとって、Lean 4を学ぶ価値はあるのでしょうか？

本記事は、こうした問いに正面から答える入門記事 です。

前提知識は要りません。

Python言語のご経験しかない、関数型プログラミングも定理証明・形式証明支援言語についてはまったく学んだことはない、という方々を想定しています。

論理学も大学数学も未習でよい前提で、すべての専門用語を初出の場で説明しながら進みます。

この記事の全体像 ── 順路と結論を最初に

結論を先に言うと

Lean 4 は、数学の主張を型として書き、その証明をプログラムとして書ける言語です。

しかも、証明を支える道具立て（タクティク） も、言語の拡張 も、すべて Lean 4 自身で書けるという徹底した自己記述の設計思想 を持ちます。

この設計と、Mathlib（マスリブ）という人類最大級の形式化数学ライブラリの存在 が、数学者の共同作業と AI の学習・検証の両方に理想的な土壌を提供 しました。

数学の形式化と AI ×定理証明の現在の主戦場は Lean 4 です
── これが本記事の 結論 です。

ここに出てきた用語は、すべて本文で説明します。

順路 ── ３部構成で進みます

第１部（基礎編）── 前提知識ゼロから、次の４段階で土台を作ります。

1.まず「定理証明系」── 数学の証明を機械が支える仕組み ── を３分で知る
2.次に、Lean 4 という言語の個性（自己記述）を知る
3.そして「型が主張になる」という考え方を、一つの例で体験する
4.最後に、Mathlib ── 数学の巨大な共有図書館 ── を知る

第２部（本編）── Lean 4 の歴史、実際に動かす体験、業務の現場（要件から証明までの４ステップと５つの事例）、数学者の５つの型、数学の最前線、AI の現場、世界の潮流と日本の現在地、ソフトウェアの現場、他言語との使い分け、の順に掘り下げます。

第３部（応用編）── 率直な問い（Rocq と Lean 4、どちらを学ぶべきか）、「機械が検査済み」を読むリテラシー、学習リソース、対話篇、発展コラム（折りたたみ）、と続きます。

同じ順路を、一枚の図にしておきます。

先行記事と姉妹記事

本記事は単独で読めます。
筆者はこれまで、形式検証の世界を別の角度から紹介してきました。

• λProlog とは何か ── AI が数学を証明する時代、定理証明系 Rocq の内側で働く知られざる言語 ── Lean 4 と並ぶ主要な定理証明系 Rocq の、内側の言語の物語です
   
• F*（F Star）とは何か ── 検証済みコードがそのまま製品で動く、もう一つの生き方です
   
• 形式証明は「仕様が人間の意図を反映しているか」は保証しない ── 本記事の対話篇に登場する２人の初出記事です

想定読者

• これまでプログラミング言語は Python だけを使ってきたエンジニア
   
• AlphaProof や「AI が数学オリンピックで銀メダル」のニュースの背景を知りたい方
   
• 定理証明系（Lean 4、Rocq、Isabelle、Agda など）を学んだことがない方
   
• 数学は好きだったが、大学数学や論理学は未習の方
   
• Lean と Lean 4 の違い、Rocq（旧 Coq）との違いが気になっている方
   
• AI と数学・形式検証の接点に関心のある方

この記事を読む価値

1. Lean 4 とは何か、なぜいま数学者と AI 研究者の主戦場なのかが分かるようになる
    
2. 「型が主張になり、プログラムが証明になる」という発想を、実際に動くコードで体験できるようになる
    
3. Mathlib という人類最大級の数学ライブラリの規模と仕組みがつかめるようになる
    
4. テレンス・タオの形式化やフェルマーの最終定理プロジェクトなど、数学の現場の最前線が分かるようになる
    
5. AlphaProof や DeepSeek-Prover など、AI ×定理証明の潮流の中での Lean 4 の位置が分かるようになる
    
6. Rocq・Isabelle・Agda・F* との違いと使い分けの軸が手に入る
    
7. AI や他人が書いた「Lean で検査済み」の成果物を受け取るときの、３つの検分点（sorry・公理・主張文）が身につく
    
8. コードのどこが自由に付けた名前で、どこが Lean 4 の決まりかを見分けられるようになり、初めてのコードでも骨格が読める
    
9. 言語の得意不得意が土台の論理・公理系と型システムでどう決まるのかを、１６言語の比較と「Lean 4 に原理的にできないこと」の種明かしまで含めて見通せる

TL;DR

（この節の専門用語は、いずれも本文で説明いたします）

• Lean 4 は、定理証明系であると同時に、汎用のプログラミング言語でもある。両者が一つの言語に統合されている
   
• 最大の個性は自己記述 ── Lean 4 のコンパイラも、証明の道具も、言語拡張も、Lean 4 自身で書かれている
   
• Mathlib は数百人の貢献者が育てる形式化数学の巨大ライブラリで、数学の共同事業としても、AI の学習と検証の土台としても機能している
   
• 実務での使い方は４ステップ ── 業務要件を言語化し、合いそうな数学構造を教養と LLM の支援で絞り込み、仮説を Lean 4 の型として書き、機械が証明または反証する
   
• 型を選ぶことは、演算の意味を選ぶこと（Nat の引き算は０で止まる）。本記事で使うタクティクは１０個だけで、応用編に一覧の付録を置いた
   
• 数学の現場では、テレンス・タオの研究の形式化やフェルマーの最終定理の形式化プロジェクトが Lean 4 で進行中
   
• AI の現場では、AlphaProof（IMO 銀メダル相当）をはじめ、証明 AI の多くが Lean 4 を答案用紙として採用している。2025年には自然言語で解く AI が IMO 金メダル水準に達したが、人間の採点者を要する自然言語の答案と、カーネルが検査する形式化された答案は別物 ── AI が証明を量産する時代ほど、機械が採点できる答案用紙の価値は上がる
   
• 「Lean で検査済み」の成果物を受け取ったら、sorry を数え、公理を数え、主張文を読む ── カーネルの保証は主張文の手前で止まり、主張文の検分は人間の仕事として残る
   
• ソフトウェア検証の伝統資産では Rocq に、製品への直結では F* に強みがあり、目的によって使い分ける。数学の形式化と AI の潮流に乗るなら、入口は Lean 4 が第一候補
   
• 言語の得意不得意は、土台の論理・公理系と型システムで原理的に決まる ── たとえば Lean 4 は証明どうしを区別しない設計ゆえに軽くて速い代わりに、複数の等しさを扱う数学（HoTT）は原理的にできず、その領域は Cubical Agda などが受け持つ
   
• Lean 4 も Mathlib も無料のオープンソース（Apache License 2.0）。日本語コミュニティ lean-ja が教科書の翻訳と勉強会を進めており、日本語だけでも学び始められる

Lean 4 の一次情報源

• Lean 公式サイト ── https://lean-lang.org/
   
• 公式ブック "Theorem Proving in Lean 4"、"Functional Programming in Lean"、"Mathematics in Lean"（いずれも公式サイトから無料で読めます）
   
• Lean 4 の GitHub リポジトリ ── https://github.com/leanprover/lean4
   
• Mathlib の GitHub リポジトリ ── https://github.com/leanprover-community/mathlib4
   
• ブラウザ実行環境 Lean 4 Web ── https://live.lean-lang.org/

---

第１部（基礎編）── ４つの土台

基礎編 その１ ── 定理証明系とは何か（３分で）

定理証明系（ていりしょうめいけい）とは、数学の証明をコンピュータの上で書き、その正しさを機械に検査させるためのソフトウェアです。

証明とは、主張が正しいことを、あらかじめ認められた推論の規則だけを使って一歩ずつ示した道筋のことでした。人間が紙の上で書く証明は、行間の飛躍や思い込みが紛れ込みます。定理証明系の上で書く証明は、一歩一歩がすべて機械に検査されるため、検査を通った主張には飛躍もごまかしも残っていません。

検査の番人はカーネルと呼ばれる小さな中核部品です。

どれほど長大な証明も、最後は必ずカーネルの検査を通らなければ定理として認められません。
この「小さな番人がすべてを最終検査する」構造は、Lean 4 でも、Rocqを取り上げた別の記事 でも共通する設計構造です。

基礎編 その２ ── Lean 4 という言語（自己記述という個性）

Lean（リーン） は、Microsoft Research の研究者レオナルド・デ・モウラが2013年に開発を始めた定理証明系です。バージョンを重ねて成長し、2023年に正式リリースされた現行版が Lean 4 です。

現在は、開発を専門に担う 非営利組織 Lean FRO が中心となって開発を主導しています。

Lean 4 の最大の個性は、徹底した自己記述にあります。

• Lean 4 のコンパイラは Lean 4 で書かれています。
• 証明を進める道具（タクティク。後述します）も Lean 4 で書きます。
• 言語の文法を拡張する仕組みも Lean 4 の中にあります。

つまり、Lean 4 を学べば、その言語を改造する言語まで同時に手に入る のです。

この点は、姉妹記事の λProlog の物語と対照的です。

Rocq は、「メタプログラミング（プログラムを操作するプログラムを書くこと）を行うために、みずからとは別の言語である λProlog を客人として迎える」という設計アプローチを選択しました。

それとは対照的に、Lean 4 は、「自分のことは、ぜんぶ自分で書く」という設計方針 を選びました。

これは、同じ課題に対して取り得る２つの設計アプローチ です。

Lean 4nには、もう一つ見逃せない個性があります。

Lean 4 は、定理証明系であると同時に、ごく普通に使える汎用のプログラミング言語でもあることです。
Lean 4で、Web サーバも、コマンドラインツールも実装することができます。

「数学の証明」と「日常のプログラミング」が、別の道具ではなくひとつの言語の２つの顔になっている
── ここが Lean 4 の設計思想の特徴です。

基礎編 その３ ── 型が主張になる（一つの例で）

Python の型ヒント int は「この変数には整数のどれか１つが入る」ことしか語れません。

Lean 4 の型は、はるかに多くを語ることができます。

「すべての自然数 $n$ について $n + ０ = n$ が成り立つ」という数学の主張そのものを、型として書けるのです。

theorem add_zero' (n : Nat) : n + 0 = n := rfl

読み方はこうです。theorem は定理の宣言。add_zero' は自分で付けた名前。

コロンの右側 (n : Nat) : n + 0 = n が型であり、同時に証明したい主張です（Nat は自然数、つまり０以上の整数の型）。

そして := rfl が証明の本体 ── rfl は reflexivity（同じものは同じ）の略で、「左辺と右辺は定義どおり計算すれば同じです」という、いちばん短い証明です。

Lean 4コードの書き方：予約語・ライブラリ名・プログラマが任意の名前を付けられる箇所

Lean 4 のコードを初めてご覧になる方のために、この最初の１行を教材にして、読み方の基本をひとつだけ身につけておきましょう。

コードに現れる語は、予約語・ライブラリ名・プログラマが任意に付けた名前のいずれかです。

この３つの区別がつくようになると、初見のコードでも骨格を追えるようになります。

• 予約語と記号：この行では theorem、丸括弧、:、:= が該当します。
  Lean 4の文法によって定められた記法ですので、一字でも変えればエラーになります。Python における def や return に相当します
   
• ライブラリ名：この行では Nat と rfl が該当します。
  もとをたどれば、Lean 4 の開発者たちがかつて任意に付けた名前が、いまではライブラリに登録されている。 そういう素性の語です。
  Lean 4のコードを記述する際は、ライブラリを１文字でも打ち間違えると、「そのような名前は知りません」とエラーになります
   
• プログラマが自由に名前を付けられる箇所：この行では add_zero' と n が該当します。
  プログラマがその場で決めた名前ですから、taro でも my_first_theorem でも構いません。
  末尾の '（アポストロフィ）も名前に使える通常の文字で、ここでは、Mathlib を読み込んだ環境に存在する add_zero というライブラリ名 と衝突しないよう、あらかじめ付けてあります

【 8/13 事後記載 】この３分類には、正確を期すためには、以下の但し書きが必要です

本記事の公開後、読者の方からこの３分類についてご指摘をいただきました。

第１に、Nat や rfl を「ライブラリ名」と呼ぶのは適切ではありませんでした。

Nat は型、rfl は定理です。これに対して Mathlib や Batteries は、ライブラリそのものの名前です。両者を同じ語で括ることはできません。

第２に、def や #eval を「予約語」として Nat と区別する根拠は、Lean 4 にはありません。

Lean 4 では、これらの構文の多くが、言語に固定された予約語ではなく、標準ライブラリの中でマクロとして定義されています。 つまり Nat や rfl と、素性としては同じものです。

本記事の後半で見るとおり、利用者が同じ仕組みで新しい構文を定義することもできます。 そこでは「自分で付けた名前が、言語の決まりの側に加わる」と述べており、この節の分類と矛盾していました。

本来は、以下のように改めるべきでした。

【 用語について 】

「ライブラリ名」という語は、すべて「ライブラリで定義された名前」と書くべきでした。
この記事には、数えられた限りで、26箇所、該当箇所があります。

「予約語」という語も、すべて「Lean 4 の構文」とすべきでした。こちらは16箇所と思われます。

（該当箇所）

見出しの 「Lean 4コードの書き方：予約語・ライブラリ名・プログラマが任意の名前を付けられる箇所」 は、「Lean 4コードの書き方：構文・ライブラリで定義された名前・プログラマが任意の名前を付けられる箇所」 とすべきでした。

「Python における def や return に相当します」という一文は、削除すべきでした。

Python の def は言語に固定された予約語ですが、Lean 4 の def はそうではありません。
この対応づけ自体が誤りです。

「そういう素性の語です」は「そういう素性の名前です」、
「add_zero というライブラリ名」は「add_zero という既存の名前」

とすべきでした。

それでもなお、本記事がこの３分類を用い続ける理由は、コードを読む際の実用上の目安となり得ると考えるためです。

「言語の中核に近く、通常はそのまま使うもの」
「ライブラリが提供する型や定理」
「その場で自由に決めた名前」

これらの分類は、厳密な境界ではなく、読解の手がかりとお考えください。

ご指摘くださった方に、感謝いたします。

ひとつ、心に留めておいていただきたいことがあります。

プログラマが任意に付けた名前は、やがてライブラリ名と同じ立場に変わります。

add_zero' も、名付けた瞬間からこのファイルの中では登録済みの名前となり、以後は正確な綴りで呼ばなければなりません。

要するに、言語の設計者が定めた語か、書き手自身が定めた語か
── 両者の違いはそれだけです。

誰が名付けたにせよ、いったん名前が付いた後は、一字の狂いも許されないのです。

本記事ではコードを示すたびに、どの語が予約語で、どれがライブラリ名で、どれがプログラマの付けた名前なのかを短く添えさせていただきます。

ところで、主張を型として書き、その型を持つ値（プログラム）を作ることが証明になる。
この対応関係には、 Curry-Howard 対応（カリー・ハワード対応） という名前がついています。

詳しくは、以下の記事をご参照ください。

λProlog とは何か ── AI が数学を証明する時代、定理証明系 Rocq の内側で働く知られざる言語

基礎編 その４ ── Mathlib（数学の巨大な共有図書館）

Lean 4 を語る上で、言語本体と同じくらい重要な存在が Mathlib（マスリブ） です。

Mathlib は、世界中の数学者とエンジニアが共同で育てている形式化された数学の巨大ライブラリです。

高校数学から大学院レベルの現代数学まで、数十万件の定理と定義が、百数十万行を超える規模で機械に検査済みの形で収められています。

貢献者は数百人にのぼり、いまも毎日成長しています。

たとえば「（a + b） の２乗の展開」のような教科書の定理はすべて収録済みです。
Mathlib を読み込めば、以下のようにコードを書くことができるようになります。

import Mathlib

example (a b : ℝ) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring

ring（リング）は「環（足し算と掛け算の世界）の等式を自動で片づけて」というタクティクで、展開も整理も機械がやります。

このコードの中では、import が予約語、Mathlib（図書館ぜんたいの名前）と ℝ（実数の型。Mathlib が定めた記号で、Real と綴っても同じ）と ring（タクティク）がライブラリ名、a と b がプログラマの付けた名前です。

数学者が Mathlib に集まる理由も、AI が Lean 4 を答案用紙に選ぶ理由も、突き詰めればこの図書館の存在bに行き着きます
── 巨人の肩が、機械に検査済みの形で公開されている のです。

---

第２部（本編）

Lean 4 の歴史 ── Microsoft Research から、コミュニティの言語へ

Lean の歩みを、駆け足でたどります。

• 2013年 ── Microsoft Research のレオナルド・デ・モウラが Lean の開発を開始。デ・モウラは、F* の相棒として姉妹記事にも登場した SMT ソルバ Z3 の作者でもあります
   
• 2017年 ── Lean 3 が公開され、数学者コミュニティによるライブラリ mathlib の成長が始まる
   
• ２０２１〜2023年 ── 言語を根本から書き直した Lean 4 が段階的に公開され、2023年に正式リリース。mathlib も全面移植され、現在の Mathlib（Lean 4 版）になる
   
• 2023年 ── 開発を専門に担う非営利の研究組織 Lean FRO が発足。Microsoft の一研究プロジェクトから、独立した基盤を持つコミュニティの言語へと歩みを進める

【 補足説明 】

ウェブ上には、Lean 3 時代の解説記事が多く残っています。

Lean 3 と Lean 4 は文法もライブラリも大きく異なるため、Leanをこれから学ぼうという皆様は、「Lean 4」と明記された資料を選んでください（本記事のコードはすべて Lean 4 です）。

なお、Lean 4 本体も Mathlib もオープンソース（Apache License 2.0）で、無料で商用利用可能です。

動かす体験 ── ブラウザで、２ + ２ = ４から帰納法まで

何もインストールせずに始める

公式のブラウザ実行環境 Lean 4 Web（https://live.lean-lang.org/）を開けば、アカウント登録もインストールも不要で、いますぐ Lean 4 を動かすことができます。

それでは、まずは肩慣らしといきましょう。

#eval 2 + 2          -- 4 と表示される
#eval "こんにちは、" ++ "Lean 4"

def double (x : Nat) : Nat := 2 * x
#eval double 21      -- 42

#eval は「計算して見せて」の命令、def は関数定義です。ここまでは普通のプログラミング言語の顔です。

このコードでプログラマが自分で名付けたのは、double と x です。

#eval、def、:=、コメント記号 -- は予約語と記号 です。
Nat と、文字列の連結 ++ は、どちらもライブラリ名 です（演算子もライブラリ名の仲間です）。

小さな罠 ── 自然数の引き算

普通の言語のつもりで触っていると、最初に驚くのがこれです。

#eval (5 - 10 : Nat)   -- 0
#eval (5 - 10 : Int)   -- -5

$Nat$（自然数） は $０$ 以上の数の型 なので、答えが負になる引き算は $０$ で止まる、と定義されています。

これはバグではなく、型の定義そのものの動作 です。

ここに大事な教訓が１つあります ── 型を選ぶことは、演算の意味を選ぶということ です。

後の「業務の現場」の節で金額の計算に $Int$（整数）を使うのは、この罠を避けるためです。

なお、(5 - 10 : Nat) の部分で、「この式を Nat として読め」という型の指定をしています。
この : の使い方も予約語と記号の仲間です。Int（整数の型）はライブラリ名です。

証明の顔 ── そして機械は忖度しない

example : 2 + 2 = 4 := rfl     -- 通る
example : 2 + 2 = 5 := rfl     -- 赤いエラー

example は、「名前を付けない定理」の宣言 です。
１行目は受理され、２行目は拒否（拒絶）されます。

この容赦のなさが、定理証明系の力の源 です。

example は予約語 で、名前を付けない宣言 ですから、このコードには、プログラマが自分で名付ける名前は登場しません。

同じ定理でも、言語が違えば景色が違う

ところで、Lean 4 と並ぶ代表的な定理証明系に Rocq（ロック。旧名 Coq（コック））があります。
「 $x + ０ = x$ 」を Rocq で証明しようとすると、rfl では終わらず、帰納法が必要になります。

理由は、足し算という関数の定義のしかた にあります。

Lean 4 の足し算は、「右側の数を一つずつ崩す」形で定義されています。

$x + ０$ なら、右側が $０$ ですから「崩すものが何もない。答えは $x$ 」と、定義を読むだけで即座に決まります。だから rfl の一言で通る のです。

Rocq の標準の足し算は、これと反対に「左側の数を一つずつ崩す」形で定義されています。

$x + ０$ の左側は $x$、つまり中身の分からない変数ですから、定義だけでは一歩も計算が進みません。

$x$ が $０$ の場合、$１$ の場合、$２$ の場合…と、すべての場合で成り立つことを帰納法で示すほかなくなります。

つまりこの差は、言語の優劣ではありません。

足し算をどちら側の引数で定義したかという言語設計の違いが、そのまま証明の手間の違いになって現れている のです。

同じ定理でも、言語が違えば見える景色が違う ── その最初の実例 です。

Lean 4 では、以下のように、 rfl と一言書けば事足ります。

theorem add_zero' (n : Nat) : n + 0 = n := rfl        -- 一言で終わる

theorem zero_add' (n : Nat) : 0 + n = n := by         -- こちらは一言では終わらない
  induction n with
  | zero      => rfl
  | succ k ih => rw [Nat.add_succ, ih]

種明かしをすると、Lean 4 の足し算は「右側の引数を分解して計算する」ように定義されているため、$n + ０$は定義どおり計算するだけで $n$ になります（だから rfl）。

ところが、左右を入れ替えた $０ + n = n$ は定義だけでは進まず、帰納法 ── 「$０$の場合を示し、$k$ で成り立つなら $k + １$ でも成り立つことを示す」という証明の型 ── が必要になります。

２つ目の証明を読み解きます。
by は、「ここからタクティクで証明します」を意味する合図です。

タクティク とは、証明の途中経過（ゴール）を一手ずつ変形していく指示のこと。

induction n with は、「$n$ について帰納法で場合分けせよ」という指示です。
zero の場合 は rfl、
succ（ $k$ の次の数）の場合は、rw（rewrite、書き換え） で式を整えた上で、帰納法の仮定 ih を使って締める
── 将棋の一手のような指示の積み重ねで、証明が組み上がっていきます。

なお、本記事に登場するタクティクは全部で１０個です。
この記事の「応用編」の末尾に、復習用に一覧表を付録として置かせていただいております。

ここではタクティクを覚えようとはせず、雰囲気だけつかんでいただけたら、先へと進んでください。

このコードで、プログラマが自分で好きな名前を付けた部分は、zero_add'、n、k、そして ih です。

ih は induction hypothesis（帰納法の仮定） の頭文字を取った名前で、Lean 4 のプログラマは慣習的にこう命名しますが、名前そのものは自由に決められますから、kasetsu と書いても通ります。

by、induction、with、|、=> は予約語と記号です。

rfl と rw はタクティクの名前です。
Nat.add_succ は、「$n + （m + １） = （n + m） + １$」という補題にライブラリ開発者が付けた名前で、いずれもライブラリ名 です。

注意が必要な部分は zero と succ です。

この２つは、一見すると自分で選べる名前のようですが、そうではありません。

$Nat$ という型 そのものが、「zero と succ という２つの作り方でできている」と定義されているため、場合分けの枝には、その定義どおりの綴りを書く必要があります。

ここを jiro などに変えると、エラーになります。

画面の中では、何が起きているのか

上の帰納法の証明を Lean 4 Web に貼ると、エディタの右側（Infoview と呼ばれる領域）に、いま証明すべき残りの主張 ── ゴールと呼びます ── が表示されます。

カーソルを１行ずつ動かすと、タクティクの一手ごとにゴールが変形されていく様子を観察できます。

succ の枝を実況すると、こうなります。

induction n with の直後:
  ih : 0 + k = k           ← 帰納法の仮定(使ってよい既知の事実)
  ⊢ 0 + (k + 1) = k + 1    ← いま示すべきゴール(⊢ の右側)

rw [Nat.add_succ] の後:
  ⊢ 0 + k + 1 = k + 1      ← 足し算の定義で、左辺を一歩だけ計算した形

rw [ih] を指した瞬間:
  No goals                 ← 仮定で書き換えたら両辺が同じ形になり、証明完了

一手指すたびに、盤面（ゴール）が変わる ── これが、対話的定理証明系の「対話」の正体です。証明を書くとは、文章を一気に書き上げることではなく、機械と盤面を挟んで一手ずつ指し進めることなのです。

もう一つ、初心者の最強の味方を紹介します。
sorry です。

theorem zero_add'' (n : Nat) : 0 + n = n := by
  sorry    -- 「ここは後で埋めます」という保留の宣言

sorry は、「この部分の証明は保留」という正式な宣言で、Lean は警告つきでいったん受け入れてくれます。

大きな証明に挑むときは、まず全体を sorry の足場で組んでおき、一箇所ずつ本物の証明に置き換えていく ── これが 定石の進め方 です。

ただし、sorry が１つでも残った定理は、当然ながら証明済みとは呼べません。

この点は、応用編でもう一度戻ってきます。

sorry は、Lean 4の言語で定義されている予約語です。

zero_add'' は、プログラマが任意に付けられる名前を記述した部分です。

上記のサンプルコードでは、すでに定義済みの zero_add' と名前が衝突しないように、' をもう１つ足して違う名前にしています。ここはまったく別の名前を付けても何ら構いません。

足場の話はここまでにして、この節で証明した２つの式をあらためて並べてみましょう。

rfl の一言で終わった「$n + ０ = n$」と、帰納法まで必要だった「$０ + n = n$」です。

数学的にはどちらも「自明」に見える２つの式が、機械から見ると難易度の違う別の問題になっています。

ここに、「定義どおり計算できること」と「証明が必要なこと」の境界線 が現れています。

この感覚がつかめたら、あなたはもう定理証明系の入口 に立っています。

図書館は、必要な本を見つけられて初めて有用な書庫になる

Mathlib に数十万の定理があっても、目当ての１つを見つけられなければ宝の持ち腐れです。
Lean 4 には、それを解決する仕組みが言語の側に備わっています。

exact? というタクティク です。

import Mathlib

example (a b : Nat) : a + b = b + a := by
  exact?    -- このゴールを閉じられる定理を、Mathlib から探して

実行すると Lean はライブラリを検索し、「exact Nat.add_comm a b で閉じられます」と提案してきます（Nat.add_comm は、足し算の交換法則の定理名 です）。

本来なら、人間がまずライブラリの中から使えそうな定理を探し出し、その名前を使って証明を書きます。

exact? では順番が逆になります。

人間は証明したい主張だけを書き、それに合う既存の定理がMathlibに存在するかどうか？
Mathlibに存在するとしたらどの定理なのかを、機械（Lean 4）が探してくるのです。

exact? はタクティクの名前です。
また、提案として返ってくる Nat.add_comm は足し算の交換法則の補題の名前で、どちらもライブラリ名です。

このライブラリ名を知らなくても機械が探し出してくれる、というのが本節の主旨です。

a と b は、プログラマが自分で名付けた名前です。

exact? は、ただの便利機能と見なすべきではありません。

実務で形式検証を使うときの基本動作は、要件を性質として言語化し、その性質を保証する既存の定理をライブラリから探す、というループ だからです。

exact? は、このループにおいて、「探す」工程を機械化してくれる有用な機能なのです。

検索を機械化・自動化してくれることで、Mathlib に定義済みの数十万以上の数学定理は、本当の意味であなたにとって有用な道具箱になるのです。

図書館は、どこの書棚にどの内容の本が所蔵されているのかという情報が整理されていて初めて、アクセスが容易な知の館に変わるのです。

業務の現場 ── 要件から証明まで、４ステップ×５つの事例

Lean 4 を業務で活用するときの手順は、次の４ステップです。

②の直感は大学数学の記憶の断片で十分ですし、心もとなければ、LLM に「この要件に対応する数学の性質は何か」と聞くことで、該当しそうな数学知識を引き出すことができます。

ここで大事なのは、LLM（AI Agent、Coding Agent）と Lean 4 との役割分担 です。

LLMからの回答は、あくまで候補であり、正しさの確定は④の機械（Lean 4）が行います。

このフローにおける各アクターの役割を整理すると、互いの弱点を補い合う関係が成り立っていることが分かります。

アクター	役割	出力の性質
人間（エンジニア）	業務要件を解釈し、対応する数学的構造の見当を付ける	抽象的なアイデアと方向性
LLM（AI アシスタント）	人間の記憶や知識を補完し、数学的性質の候補を提示する	確率的で柔軟なヒント（誤りを含む可能性がある）
Lean 4（定理証明系）	提示された候補に対し、論理的な正しさを確定する	絶対的な真偽（証明の受理または拒絶）

抽象的な説明が続きました。

ここからは、具体的なイメージをつかんでいただくために、５つの事例を挙げてみたいと思います。

これから見ていただく５つの事例は、上記の４つの工程からなる実務手順（ステップ）を体感していただくために筆者が構成した例題です。

Lean 4のコードは要点のみを記載します。

コードは、Lean 4 Web にそのままcopy & pasteしていただくことで、実際に動かすことができます
（この節のコードは Mathlib の読み込みも不要です）。

事例１（小売）── 割引は、どちらを先に適用してもよいか

① 業務要件
──「クーポン割引（１００円引き）と会員割引（２００円引き）は、適用の順序によらず最終価格が同じであること」。

② エンジニア（人間）の直感
── 「順序を入れ替えても結果が同じ」 は、数学では、交換（可換）と呼ばれる性質です。

自信がなければ LLM にこう尋ねてみることができます。
──「適用順序によらず結果が同じ、という要件に対応する数学の性質の名前は？」。

③④ 形式化と判定 ──

「形式化」とは、②で見当を付けた数学的性質を、機械が検査できる Lean 4 のコードとして書き下すこと です。

theorem discount_comm (price : Int) :
    (price - 100) - 200 = (price - 200) - 100 := by
  omega

**omega（オメガ）**は、整数の足し算・引き算・大小比較（線形算術と呼ばれる範囲）の主張を自動で判定してくれるタクティク です。

コンパイルが通った瞬間に、この要件は、「すべての価格について」証明 されました。

なお、価格の型に Int を選んだのは、「動かす体験」の節で見た 自然数の引き算の罠を避けるため です。

このコードでプログラマが自分で名付けたのは、discount_comm と price です。

**Int（整数の型）**と omega は、どちらも ライブラリ名 です。

事例２（物流）── ２便に分けても、重量合計は合うか

① 業務要件
──「荷物を２便のトラックに分けて積んだとき、便ごとの重量合計の和が、全体の一括合計と一致すること」。

② エンジニア（人間）の直感
── 「分けて足しても、まとめて足しても同じ」 は、足し算の結合律 の仕事です。

LLMへの尋ね方の例
──「リストを分割して集計しても結果が変わらないために、演算が満たすべき性質 は？」。

③④ 形式化と判定

def total : List Int → Int
  | []        => 0
  | w :: rest => w + total rest

theorem total_append (l1 l2 : List Int) :
    total (l1 ++ l2) = total l1 + total l2 := by
  induction l1 with
  | nil => simp [total]
  | cons w rest ih => simp [total, ih, Int.add_assoc]

def の２行は、「空のリストなら $０$。先頭 w と残り rest に分けて w + 残りの合計」という定義です。

| による場合分けは、「動かす体験」の節の induction と同じ形です。

証明はリストについての帰納法で、simp（シンプ） は 「渡した等式を使って両辺を整理せよ」というタクティク です。

ここでは、total の定義 と 帰納法の仮定 ih と、整数の足し算の結合律 Int.add_assoc を渡しています。

このコードでプログラマが自分で名付けたのは、total、w、rest、l1、l2、ih です。

def、|、=> は予約語と記号です。

List（リストの型）、++（リスト連結の演算子）、simp、Int.add_assoc（整数の結合律）は、いずれもライブラリ名 です。

nil と cons には注意が必要 です。

List という型は、「nil（空のリスト）と cons（先頭に要素を１つ加えたリスト）の２つから組み立てる」と定義 されており、この２つは その定義に登録された名前 です。

そのため、場合分けの枝にはこの綴りをそのまま書く必要があります。

Nat の帰納法で見た zero・succ と同じ、一見すると自分で選べるようで実は選べない名前です。

コラム：cons と nil に見覚えのある方へ ── Lisp から続く関数型言語の系譜（クリックで開閉）

Lisp を学んだことのある方なら、cons という名前に懐かしさを覚えたかもしれません。

cons は、１９５０年代末に生まれた言語 Lisp で、「先頭に要素を１つ加えてリストを組み立てる」操作に付けられた名前 です（ construct に由来 します ）。

空のリストを nil と呼ぶ流儀も Lisp が広めたもの です。

リストを「空か、先頭＋残りか」の２通りで組み立てるという考え方そのものが、Lisp が確立し、後の関数型言語たちが受け継いできた共有財産なのです。

Lean 4 は、この系譜の上に立つ言語です。

直接の設計は ML や Haskell といった 関数型言語の流れ を汲んでいます。

| で場合分けしながら定義を書く文法、関数を値として渡せる仕組み、再帰でリストを処理する発想は、いずれもこの一族に共通のものです。

List の枝の名前が cons と nil なのは、半世紀以上前の Lisp から関数型言語の家系図をたどって届いた語彙、というわけです。

Pythonエンジニアの方々には、逆にこう考えると腑に落ちるかもしれません。

── Python の for 文で先頭から１つずつ処理する感覚を、Lean 4 では「先頭（cons の頭）と残り（rest）に分けて、残りに同じ処理を繰り返す」という再帰の形で書いている、と。

同じ仕事の、別の流儀です。

事例３（SaaS）── 管理者は、閲覧もできるか

① 業務要件
──「権限レベル２以上（管理者）の利用者は、レベル１以上を要求する閲覧機能を必ず使えること」。

② エンジニア（人間）の直感
── 権限の 包含 は、数の大小（順序） に写すことができます。

LLMへの尋ね方の例

──「上位権限が下位権限の操作を必ず含む、という性質は、数学の言葉（構造）で表現すると、どう表せる？」。

③④ 形式化と判定

theorem admin_can_view (level : Nat) (h : 2 ≤ level) : 1 ≤ level := by
  omega

新しい形が１つあります。

引数の (h : 2 ≤ level) は、「$２≤ level$ という前提に h という名前を付けて 受け取る」という書き方です。「〜のときに限り」という条件付きの主張 は、この形で書きます。

前提すら名前付きの値として扱う
── ここにも、「主張は型、証明は値」の思想 が顔を出しています。

このコードでプログラマが自分で名付けたのは、admin_can_view、level、そして前提に付けた h です。

≤（小なりイコール。記号もライブラリ名の仲間です）と omega は、どちらもライブラリ名 です。

事例４（会計）── 明細ごとの端数処理は、合計と一致するか（反証の例）

① 業務要件（という名の仮説）
──「税額計算は、明細ごとに計算して合計しても、合計額に対して計算しても一致するはずだ」。

② エンジニア（人間）の直感
── 成り立つなら、分配法則の親戚 です。
ただし、切り捨て（整数除算）が絡むと怪しい という嗅覚も大学数学の教養のうちです。

③④ 形式化と判定

def tax (price : Nat) : Nat := price * 10 / 100

example : tax 5 + tax 5 ≠ tax (5 + 5) := by decide

decide（ディサイド）は「有限の計算で白黒つく主張は、計算して判定せよ」というタクティクです。

tax 5 は、$５０÷１００$ の切り捨てで $０$、tax 10は $１$ 。
よって、$０ + ０≠１$ が成り立ちますから、 この example は、「一致するはず」という仮説への反例が存在することの証明 になっています。

ここでもしも、「すべての価格で一致する」という定理を書いていたら、Lean 4 は決してこの証明を受理せず、エラーを返し続けます ── 機械が仮説を棄却したのです。

反証された後の分岐は、人間の仕事です。

業務要件を変える（例えば、端数は常に合計額ベースで計算すると業務ルールを決める）か、モデル（対応する数学的構造）を探しなおす（一致ではなく「差は明細数未満」という弱い保証に書き換える）か。

Lean 4が担ってくれるのは、矛盾を突きつけるところまでです。

決断は業務（についてドメイン知識）を知る人間が担うべき仕事である。
（要件を変えることに伴う業務への影響がもたらす弊害や利益は、人間が責任を持って判断するべきです）
── この分担が、形式検証を実務で使うときの原則になります。

このコードでプログラマが自分で名付けたのは、tax と price です。

def と example は予約語です。

* と /（自然数の割り算は切り捨て、という定義ごと登録されています）、≠（等しくない）、decide は、いずれもライブラリ名 です。

事例５（ヘルスケア）── 換算しても、優先順位は崩れないか

① 業務要件
──「トリアージの点数を別尺度に換算する（３倍して２を足す）とき、患者間の優先順位が入れ替わらないこと」。

② エンジニア（人間）の直感
── 順序を壊さない変換には単調（たんちょう）という名前があります。

LLM への質問例
──「大小関係を保存する関数の性質を何と呼ぶ?」。

③④ 形式化と判定

theorem score_mono (a b : Nat) (h : a ≤ b) :
    3 * a + 2 ≤ 3 * b + 2 := by
  omega

このコードでプログラマが自分で名付けたのは、score_mono、a、b、h です。

omega はライブラリ名です（３倍のような定数倍までは、線形算術の守備範囲に収まります）。

事例を通して確認したこと

ここまで、皆様と５つの事例を見てきました。

ここで、５つの事例を貫く共通点 を振り返ってみたいと思います。

コードはどれも数行で、証明はほぼ、Lean 4が済ませてくれました。

人間が担うべき役割 は、「ステップ① 業務要件の言語化」と「ステップ② 構造の見当」、そして、「ステップ④の、反証されたときの対処策を見極める意思決定」の３箇所に濃縮されています。

これらの３箇所は人間の持ち場 です。

しかし、人間が独力でこなす必要はありません。

それぞれの場面で、LLM ── Claude Code のような Coding Agent ── が支援役に付いてくれる からです。

「ステップ① 業務要件」を言語化する工程 では、LLMは、曖昧さの検査役になります。

書き上げた要件文を渡して、「この要件に曖昧な箇所や、暗黙の前提はないか」と尋ねれば、「『適用の順序によらず』とありますが、割引が３種類以上になった場合も含みますか」といった見落としを指摘してくれます。

形式化は曖昧さを許さない ので、この段階で言葉を締めておくほど、後の工程が楽になります。

「ステップ② 数学的構造の探索」の工程 では、LLMは、数学構造の候補を探りあてて、理由付きで提示してくれます。

数学の教養が、実務において威力を発揮するのは、公式の暗記ではなく、ステップ②の業務要件に対応する数学構造を探りあてる場面なのです。

そして、AI Agent（LLM）がこのステップを知識面・探索力（検索力）で手助けしてくれます。

「この業務要件に対応する数学の性質は何か？」 とLLMに尋ねれば、LLMは、候補となる数学構造が存在するかどうか、存在する場合は、候補となる数学構造の名前（数学用語）と、その数学構造が業務要件にどう対応するのかを説明してくれます。

業務要件を追加すれば、対応する数学構造の候補も、絞り込まれていきます。

分からない用語を、LLMにその場で壁打ちして、納得いくまで聞き返すことができます。

LLMは、人間の記憶の断片を補う相談相手です。

「ステップ④」の対処策の意思決定の工程 では、判断材料の整理役 になります。

業務要件に対応するという仮説を立てた数学構造が、Lean 4によって反証されたとき、「要件側を変える対処方法と、モデル（数学構造）を探し直す対処策の、どちらを目指すべきか。

それぞれの影響を整理してほしい」とLLMに質問すると、改修範囲、顧客への見え方、会計処理との整合といった検討軸を、LLMが論点整理してくれます。

しかし、論点整理された判断軸・検討軸の重要性をどう判断するか、最終的にどちらの道を選ぶかを決めるのは、業務に対して責任を持つ人間が担うべき仕事であり続けます。

つまり、LLMが担う支援の形は３箇所で少しずつ違います。

• ステップ① : LLMは、 検査役
   
• ステップ② : LLMは、候補となる数学構造の提示役
   
• ステップ④ : LLMは、論点整理役

工程	LLM の役割
ステップ①（業務要件の言語化）	曖昧さの検査役
ステップ②（数学的構造の探索）	候補となる数学構造の提示役
ステップ④（対処策の意思決定）	論点整理役

そして、どの場面でも、LLMの出力結果は、そのまますぐに採用されません。

②の候補は Lean 4 が白黒を付け、①と④の助言は人間が採否を決めるからです。

役割分担の原則は、LLMによる支援が手厚くなっても変わらないのです。

数学者の５つの型 ── 数学の現場への入門

同じ道具を、数学者はどのように使いこなしているのでしょうか。

数学者は、毎回ゼロから証明を書き上げているわけではありません。
実際には、いくつかの定石を組み合わせて、日々の証明を進めています。

本節では、その定石を５つに整理して紹介 します。

次節の巨大プロジェクトへ行く前に、その５つの定石を最小のコードで見ておきます（いずれも冒頭に import Mathlib が必要です）。

定石１ ── Mathlib に登録済みの数学定理は、Lean 4 のコードを一行書くだけで呼び出せる

example (n : ℕ) : Even (n * (n + 1)) := Nat.even_mul_succ_self n

by がありません。タクティクで組み立てる代わりに既製の証明（という値）を := の右に直接渡しています ── 基礎編その３の「証明はプログラム（値）」が、ここで文字どおりの意味になります。

このコードに出てくる ℕ（Nat を表す Mathlib の記号）、Even（偶数である、という述語）、Nat.even_mul_succ_self（この定理に付けられた名前）は、いずれもライブラリ名 です。

プログラマが自分で名付けたのは n だけです。

定石２ ── 有限の計算で白黒がつく主張は、計算タクティクに判定させる

example : Nat.Prime 101 := by norm_num

norm_num（ノルムナム） は、数値に関する主張を自動で証明してくれるタクティクです（１０１程度の小さな数なら、decide でも証明できます）。

このコードに出てくる Nat.Prime（素数である、という述語）と norm_num は、どちらもライブラリ名 です。

定石３ ── 歴史に名高い有名定理も、Mathlib の定理名ひとつで呼び出せる

「２の平方根は無理数である」── 古代ギリシアで発見された、数学史上もっとも有名な定理のひとつです。

整数の比（分数）では決して書き表せない数が存在するという事実は、発見当時の数学観を揺るがしたと伝えられ、現代でも大学入試の証明問題の定番です。

背理法を使った証明 をご記憶の方もいらっしゃるのではないでしょうか。

この歴史的な定理を Lean 4 で証明したいときは、次の一行で済みます。

example : Irrational (Real.sqrt 2) := irrational_sqrt_two

コードの読み方は、定石１とまったく同じ形です。

証明したいと言っても、自分で証明を組み立てる必要はありません。

: の右側の「Irrational (Real.sqrt 2)」が主張で、:= の右側がその証明
── そこに書かれているのは、irrational_sqrt_two という定理名ひとつだけ です。

この定理の証明は Mathlib の中で完成済みです から、名前を書いて呼び出せば、それがそのまま検査済みの証明として通用する のです。

このコードに出てくる Irrational（無理数である、という述語）、Real.sqrt（平方根）、そして定理名 irrational_sqrt_two は、いずれもライブラリ名 です。

irrational_sqrt_two という名前は、見た目こそプログラマが自分で付ける名前と変わりませんが、Mathlib の開発者たちが命名してライブラリに登録した、正確な綴りでしか呼び出せない名前です
── 基礎編その３で述べた「名付けられた後は、すべての名前が正確な綴りを要求する」の実例です。

数千年にわたり積み上げられてきた数学が、検査済みの部品として、Mathlibの棚に並んでいる
── Mathlib とは何かという問いへの答えが、この一行に凝縮されています。

定石４ ── 自作した定義についての定理は、帰納法で証明する

def oddSum : Nat → Nat
  | 0     => 0
  | n + 1 => oddSum n + (2 * n + 1)

theorem oddSum_sq (n : Nat) : oddSum n = n * n := by
  induction n with
  | zero => rfl
  | succ k ih => simp [oddSum, ih]; ring

「動かす体験」の節の帰納法と「業務の現場」の節の simp と基礎編その４の ring が、ここで合流しました。

succ の枝では simp が定義と仮定で式を整え、残った展開の等式「 $k × k + （2k + １） = （k + １）×（k + １）$ 」を ring が閉じます。

このコードでプログラマが自分で名付けたのは、oddSum、oddSum_sq、n、k、ih です。

定石５ ── 人間のひらめきをヒントとして渡し、残りの計算は機械に任せる

example (a b : ℝ) : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
  nlinarith [sq_nonneg (a - b)]

nlinarith（エヌリナリス） は、非線形の不等式を扱うタクティク で、角括弧の中が人間からのヒントです。

sq_nonneg（２乗は０以上である、という Mathlib の定理名） に $a − b$ を渡します。

平方完成に気づくのは人間の仕事です。
それを受けた後の式の組み立ては機械（Lean 4）の仕事です。
── 数学者の証明における分業を、１行に圧縮した定石です。

このコードでプログラマが自分で名付けたのは、a と b です。

ℝ、^（べき乗）、nlinarith、sq_nonneg は、いずれもライブラリ名 です。

５つの定石に共通しているのは、「方針とひらめきは人間が出し、検査と計算は機械が担う」という分業です。

そして驚くべきことに、次節で見る数学の最前線の巨大プロジェクトも、この５つの定石の膨大な積み重ねでできています。

数学の最前線 ── タオ、リキッド・テンソル、そしてフェルマー

Lean 4 が数学者の共同作業の場になっていることを示す、３つの実話を紹介します。

１つ目 ── リキッド・テンソル実験。2020年、現代数学の最前線を走るペーター・ショルツェが「自分の最新の定理の証明を、誰か形式化できるか」と挑戦状を出しました。証明が難解すぎて、人間の査読だけでは不安が残る、というのが動機です。

世界中の協力者が Lean の上で作業し、約１年半で形式化が完了。最先端の数学でも機械検査が届くことを示した、歴史的な共同作業になりました。

２つ目 ── テレンス・タオの実践。フィールズ賞受賞者のタオは、2023年に自らが共著で証明した最新の結果（PFR 予想の解決）を、発表からわずか数週間で Lean 4 上に形式化するプロジェクトを主導しました。

以後もタオは、大規模な共同形式化プロジェクトを次々と立ち上げ、「論文を書いたら、形式化する」という研究スタイルを自ら実演しています。

３つ目 ── フェルマーの最終定理。

「３以上の整数 $n$ について、$x^n + y^n = z^n$ を満たす正の整数の組は存在しない」
── ３５０年以上人類を退け、1995年にようやく証明されたこの定理を、Lean 4 で完全に形式化するプロジェクトが2024年に英国で始動しました。

完了まで年単位の歳月が見込まれる、数学の形式化の最高峰への挑戦です。

３つの実話に共通するのは、形式化がもはや一人の作業ではなく、Mathlib という共有図書館の上での大規模な共同事業になっている、という点です。

ソフトウェア開発の世界が経験してきたオープンソースの共同作業の文化が、数学に移植されつつあるのです。

AI の現場 ── AlphaProof と、答案用紙としての Lean 4

この記事の冒頭でご紹介したニュースに戻ります。

2024年、Google DeepMind の AlphaProof は国際数学オリンピックの問題で銀メダル相当の成績を収めました。

その仕組みを一言でいえば、「Lean 4 で答案を書き、Lean 4 のカーネルに採点させながら学ぶ AI」です。

AI が自然言語で数学の答案を書くと、もっともらしい誤答（ハルシネーション）を人間が見抜かなければなりません。

ところが答案を Lean 4 で書かせれば、正しい証明だけがカーネルの検査を通ります。
合格した答案は１００パーセント正しく、不合格の答案はどこで失敗したかの情報ごと AI の学習に回せます。

機械検査が、AI にとって最高の教師になるのです。

この構図に気づいたのは DeepMind だけではありません。

DeepSeek-Prover の系列、検索で定理を補強する型、長考型
── 近年の証明 AI の多くが、答案用紙として Lean 4 を採用しています（各プロジェクトの方式の違いは、姉妹記事で整理しました）。

理由は本記事でここまで見てきたことの裏返しです。

Mathlib という 巨大な学習素材 があり、検査が速く、答案の正しさをカーネルが保証してくれる。

AI研究者から見た Lean 4 は、教材と採点者が一体になった理想の教室 なのです。

2025年の続き ──「自然言語で金メダル級」の後で

この物語には、2025年に大きな続きが生まれました。同年７月の国際数学オリンピックで、DeepMind の Gemini Deep Think が６問中５問を解いて３５点を取り、公式に金メダル水準と認定されたのです。

しかも前年の AlphaProof と違い、人間の受験者と同じ4.5時間×２の条件で、形式言語を使わず、自然言語だけで答案を書きました。

OpenAI も実験的モデルで同じ３５点相当を報告しています。
（こちらは公式参加ではなく、元メダリストによる自社評価です）

ここで当然の疑問が生まれます
── 自然言語で金メダル級に解けるなら、Lean 4 への形式化は、もう要らないのではないか?

筆者の答えは、むしろ逆です。

第１に、採点者の問題があります。
2025年の答案は、人間の専門家が読んで採点しました。

オリンピックの数問ならそれで足りますが、数百ページの研究証明や、AI が今後毎日量産する膨大な証明を、人間の採点で捌くことはできません。

第２に、自然言語の証明には、もっともらしい誤り（ハルシネーション）が混ざる弱点が残ります。
金メダル級の答案の中にも、人間の採点者が見抜くべき危うい行間はありえます。

つまり２つの潮流は競合ではなく、分業に向かうはずです。

自然言語で発想し、Lean 4 で検査する。

AI が証明を大量に生み出す時代になるほど、機械が採点できる答案用紙の価値と、応用編で述べる「検査済みを読む」検分の技術は、むしろ重みを増していくのです。

AlphaProofの狙い ── 数学は「検証可能な訓練場」

前の節（AI の現場）の続きとして、各プロジェクトの目的をもう一段階、掘り下げて見てみましょう。

表面の目標は分かりやすいです。
オリンピックの次は研究の最前線に横たわる数学問題、いつかは未解決問題。

しかし、なぜ各社はそこまで数学に取り組むAIに投資するのでしょうか。

鍵は、AI の訓練の仕組みにあります。

AlphaProof は、囲碁で人間を超えた AlphaZero の直系です。

AlphaZero が自己対戦だけで強くなれたのは、勝敗を機械が自動判定できたからでした。

数学は、同じ構造を持つ稀有な知的領域です。
── Lean 4 のカーネルが、答案の正誤を即座に、無償で、間違いなく判定してくれる。

人間のお手本データが尽きても、機械採点を報酬にして自己改善を続けられるのです。

つまり各社が数学で磨いているのは、数学の実力そのものである以上に、幻覚のない推論エンジンを自動で鍛える方法だと言えます。

つまり、囲碁の自己対戦AI と、Lean 4 の検証結果を学習データにする定理証明AI との共通点は、次の一点にあります。

結果の良し悪しを機械（Lean 4）が自動で判定できるからこそ、人間のお手本データが尽きた後も、AI は自己改善を続けられる

この構造こそが、両者を貫く同じエンジンなのです。

反例の発見を機械が担った実例は、すでに公表されています。

Google DeepMind が２０２３年に発表した FunSearch は、LLM にプログラムを書かせては評価する探索を繰り返す仕組みで、組合せ論の未解決問題キャップセット問題において、それまで人類が知らなかった、より大きな構成を発見しました。

発見の中身が「この大きさの構成は存在しないだろう」という予想への反例として働く
── まさに仮説を棄却する側の成果です。

後継の AlphaEvolve（２０２５年発表）は、行列積の計算方式をはじめとする数学とアルゴリズムの複数の問題で、既知の記録を破る構成を自動発見したと報告されており、数学者が立てた「これが限界だろう」という見立てを、機械が構成の提示によって覆すという営みが、実務のパイプラインとして回り始めています。

FunSearch と AlphaEvolve は、Lean 4 のような定理証明系を使わないシステムです。

定理証明系なしで、どうやって正しさを確かめるのか。
答えは、扱う問題の性質にあります。

これら２つのシステムが探しているのは、証明ではありません。
「条件を満たす実物の例」です。

キャップセット問題なら「この条件を満たす、これだけ大きな集合が実際にあります」という集合そのもの、行列積なら「この手順なら掛け算の回数がこれだけ少なくて済みます」という計算手順そのものを、現物として提示するのです。

現物が提示されれば、その良し悪しは検査プログラムを実行するだけで白黒がつきます。

提示された集合が本当に条件を満たしているか、提示された手順が本当に正しい答えを返すか
── 計算機で数え上げて確かめればよいからです。仕組みとしては、LLM に候補を大量に書かせ、検査プログラムが自動で採点し、成績の良い候補を残して次の世代を生み出す
── この改良のループを膨大な回数くり返して、人類の記録を超える例に到達しました。

つまり、採点者が Lean 4 のカーネルから専用の検査プログラムに置き換わっているだけで、骨格は AlphaProof と同じです。

ただし違いもあります。

検査プログラムが確かめられるのは「この例は条件を満たす」という目の前の事実までで、「これより良い例はどこにも存在しない」という、すべての可能性にわたる主張を保証することはできません
── そこから先が、定理証明系の領分です。

その定理証明系の領分、つまり Lean 4 そのものを使った反証の実例が、中国発の取り組みにあります。

DeepSeek-Prover（２０２４年）は、Lean 4 で証明を書くAIを訓練するために、大量の数学問題を Lean 4 の命題へ自動で翻訳して、訓練データを作りました。

ただし、自動の翻訳には誤りが混ざります。

そこで彼らが採った品質管理の方法が、Lean 4 を使った選別でした。

各命題について、命題そのものと、その否定の両方の証明を AI に試みさせるのです。

否定のほうが Lean 4 のカーネルの検査を通ってしまったら、その命題は偽 ── つまり翻訳が間違っていた ── と機械的に判定し、訓練データから除外します。

反証を、データの品質を保つフィルタとして生産工程に組み込んだ形で、「仮説を機械が棄却する」営みが、毎日回る量産工程の部品になっている実例です。

学ぶ人口は、今後増えるのか

増える、というのが筆者の予想です。

理由は２つあります。

第１に、教育と研究への投資です。

米国ではカーネギーメロン大学に形式数学の研究拠点が設けられ、国防高等研究計画局（DARPA）も数学研究を AI で加速する研究計画を打ち出しました。

欧州ではインペリアル・カレッジの学部教育や、ボン大学での実践（数学の最前線の節のリキッド・テンソル）が先行しています。

第１に、教育と研究への投資が始まっています。

米国ではカーネギーメロン大学に形式数学の研究拠点が設けられ、国防高等研究計画局（DARPA）も数学研究を AI で加速する研究計画を打ち出しました。

欧州ではインペリアル・カレッジの学部教育や、ボン大学での実践（数学の最前線の節のリキッド・テンソル）が先行しています。

第２に、参入コストの急落があります。

定理証明を学び始めるためには、かつては専用の環境を確保し、専門書の理解が前提とされてきました。
これらの条件は、大学の研究室で学ばないと、容易に満たすことができない高いハードルでした。

しかし2026年8月現在、ブラウザで動く Lean 4 Web と、AI エージェントの伴走（業務の現場の節）を得ることができます。

特別な環境構築なしで、その日のうちに最初の証明を書くことが可能となったのです。

とはいえ、定理証明エンジニアの人口が、Python エンジニアの規模感まで増えることは考えにくいです。

むしろ、書ける人が少ないままで、証明を求める仕事は現に存在する。
この定理証明エンジニア人材市場の需給関係が維持されるかぎり、定理証明を書ける人材の価値は、これまで以上に高まっていくと筆者は予想します。

日本は、立ち遅れているか

率直に言えば、国家規模の投資や大学の講義数では、米中欧に見劣りするのが現状だと筆者は見ています。

しかし、空白ではありません。

第１に、本記事の冒頭で紹介した LANA プロジェクト ── IUT 理論の検証という、世界の数学界が注視する旗艦プロジェクトが、日本発で走っています。

第２に、lean-ja の草の根 ── 教科書の翻訳と勉強会が、日本語だけで学び始められる環境を整えつつあります（応用編その３）。

第３に、この分野の雇用と参加の機会は、国境をあまり選びません。

形式化プロジェクトの多くは GitHub 上に開かれていて、日本にいながら Mathlib に貢献することも、今日から可能です。

つまり日本の遅れは、決定的な差ではなく時差だ、と筆者は考えます。そして時差を縮めるのは、国家予算より先に裾野です。

この記事を読み終えたあなたが、Natural Number Game を開くかどうか。その一歩の積み重ねが、答えになります。

• Natural Number Game（https://adam.math.hhu.de/#/g/leanprover-community/NNG4） ── ブラウザで遊べる証明パズル。ゲーム感覚で帰納法まで身につく、世界的な定番教材です。ウェブ検索で見つかる旧 Lean 3 版ではなく、この Lean 4 版をお使いください。

Natural Number Game は、ブラウザで遊べる証明パズルの世界的な定番教材です。

ペアノの公理から自然数を再構築しながら、Lean での定理証明の基礎をゲーム感覚で学ぶ内容 で、公式にも「Lean への最初の入門に最適」と位置づけられています。

元々は、Lean 3 向けに設計された教材で、現在の版はケビン・バザードらの原版のアイデアに基づいて Lean 4 へ移植され、デュッセルドルフ大学の開発チームが作った Lean 4 Game Engine の上で公開されています。

検索で見つかる旧 Lean 3 版ではなく、必ずこの Lean 4 版をお使いください。

ソフトウェアの現場 ── 汎用言語としての Lean 4

「数学と AI の話は分かった。ではソフトウェアエンジニアの実務には関係あるのか」── 正直に答えます。

ソフトウェア検証の実績の厚みでは、CompCert（検証済み C コンパイラ）の伝統を持つ Rocq や、Firefox・Linux で稼働する検証済みコードを生んだ F* に、現時点では一日の長があります。

そのうえで、Lean 4 のソフトウェア側の顔も着実に育っています。代表例が、Amazon の認可ポリシー言語 Cedar（シーダー）です。

「誰がどのリソースにアクセスできるか」を記述するこの言語の設計では、仕様の数学的モデルを Lean 4 で書き、その性質を証明しながら実装を進める、という検証駆動の開発が採用されました。

クラウドのアクセス制御という、間違いが許されない領域で Lean 4 が選ばれた事実は、この言語の実務適性を示す一例です。

また、忘れてはならないのが「Lean 4 自身が Lean 4 で書かれている」という事実です。コンパイラという大規模で複雑なソフトウェアが Lean 4 で実用的に書けている以上、汎用言語としての地力は実証済みといえます。

関数型プログラミングの表現力と、必要なら証明まで書ける拡張性 ── この組み合わせに魅力を感じるエンジニアにとって、Lean 4 は「数学者の道具」を超えた選択肢になりつつあります。

その「普通の言語」の顔も、実物で確かめておきましょう。

def main : IO Unit :=
  IO.println "Hello from Lean 4!"

どの言語にもある、いちばん普通のプログラムです。IO Unit は「外の世界への働きかけ（入出力）を行う処理」の型で、画面表示のような副作用まで型で語るのが、関数型言語としての Lean 4 の顔つきです。このコードは C 言語を経由してコンパイルされ、通常の実行ファイルとして動きます。

main という名前は、仕組みのうえではプログラマが自分で名付ける名前と同じ扱いです。

ただし「実行の入口となる関数はこの綴りにする」という取り決めがあるため、プログラムとして実行したければ main と名付けます。

IO、Unit、IO.println は、いずれもライブラリ名 です。

最後に、自己記述の看板に小さな実物を添えておきます。

Lean 4 では、言語の文法そのものを数行で拡張できます。

macro "twice " x:term : term => `($x + $x)

#eval twice 21    -- 42

macro の１行は「twice という新しい書き方を、この形の式に展開せよ」という、文法への追加です。たったこれだけで、Lean 4 に twice という表現が生まれました。そしてこの同じ仕組みの上に、タクティクも、数学記号の表記も、Lean 4 の言語機能の多くも作られています。

「自分で自分を書く」は宣伝文句ではなく、日々の開発の実装方式そのものなのです。

macro、term、=>、そして構文を組み立てる引用記号 `( ) は、予約語と記号です。

x と twice は、プログラマが自分で名付けた名前です。注目していただきたいのは、ここで起きている逆転です ── プログラマが自分で付けた twice という名前が、この行を書いた瞬間から、新しい文法の一部になっています。

自分で付けた名前が、言語の決まりの側に加わる ── 自己記述の言語ならではの光景です。

使い分け ── Rocq・Isabelle・Agda・F* との比較

主要な定理証明系の中での Lean 4 の位置を、一枚にまとめます。

	Lean 4	Rocq（旧 Coq）	Isabelle	Agda	F*
ひとことで	数学と AI の主戦場	ソフトウェア検証の伝統	自動化と大規模検証	型と証明の純粋体験	製品に直結する検証
数学ライブラリ	Mathlib（最大級）	mathcomp	AFP	agda-stdlib	数学面は限定的
メタプログラミング	Lean 4 自身で	λProlog/ELPI を迎える	ML の系譜	限定的	タクティクは限定的
特筆すべき実績	IMO 銀（AlphaProof）、タオの形式化	CompCert、四色定理	seL4（OS カーネル検証）	型理論研究の標準	Firefox・Linux の暗号

この表で「メタプログラミング」の行に注目してください。

Lean 4 は自分自身で自分を拡張し、Rocq は λProlog という客人を迎える ── 同じ課題への２つの設計解であり、この対比の意味は姉妹記事で詳しく論じました。

第３部（応用編）

応用編 その１ ── 率直な問い:Rocq と Lean 4、どちらを学ぶべきか

筆者の記事群を読んでくださった方から、必ず出る問いでしょう。逃げずに答えます。

数学の形式化がしたい、AI ×定理証明の潮流に乗りたい、コミュニティの勢いを重視したい ── なら Lean 4 から始めるのが現在の第一候補です。Mathlib の規模、学習リソースの充実、証明 AI の対応状況、どれをとっても入口として恵まれています。

ソフトウェア検証の伝統資産（CompCert の系譜）に触れたい、タクティクや拡張を専用言語で書く設計思想に興味がある、λProlog という希少な言語の実務の現場を見たい ── なら Rocq です。

そして本音を言えば、この２つは「どちらか一方を選んで生涯を捧げる」ものではありません。型が主張になり、プログラムが証明になる、という核心は共通です。片方で身につけた感覚は、もう片方でそのまま通用します。

目的が決めてくれますし、目的が変われば乗り換えも難しくありません。本記事で Lean 4 の入口に立ち、姉妹記事で Rocq の内側を覗く ── 両方の景色を知っていることが、いちばんの財産になります。

応用編 その２ ──「機械が検査済み」を読むリテラシー

これからの時代、あなたが Lean 4 のコードを書く機会より先に、読む機会のほうがやってくるかもしれません。AI が生成した証明、同僚が書いた検証、ネット上の形式化 ──「Lean で検査済み」と添えられた成果物を受け取ったとき、何を確認すればよいのか。

本記事で筆者がいちばん伝えたい実践知として、３つの検分点を挙げます。

１つ目 ── sorry は残っていないか。「動かす体験」の節で紹介したとおり、sorry は「証明は保留」の宣言です。sorry を含んだままでもファイル全体は警告つきで通ってしまうため、「エラーが出ていない」ことと「証明が完了している」ことは別物です。

２つ目 ── 何を公理として仮定しているか。Lean には、証明なしで主張を真と認める axiom という仕組みがあります。それ自体は正当な道具です（証明が長大な既知の定理を仮定として置き、本題を先に進める、といった使い方があります）。

ただし、その成果物の保証は「置いた公理が正しければ」という条件付きになります。幸い、Lean 4 には確認の道具が用意されています。

#print axioms zero_add'

この一行で、その定理が依存している公理の一覧が表示されます。sorry で埋めた定理は、ここに sorryAx という名前が現れます ── つまり１つ目の検分も、この一行が兼ねてくれます。

#print axioms は **予約語（コマンド）**で、
sorryAx は ライブラリ名、
zero_add' は、プログラマが自分で名付けた名前（の参照） です。

３つ目 ── これた最も重要です。

主張（命題）そのものは、意図どおりか。
カーネルが保証してくれるのは「書かれた主張に、規則どおりの証明が付いている」ことまでです。

その主張が、皆様確かめたかったことと一致しているかどうかは、カーネルには判定できません。定理の名前がどれほど立派でも、主張文が空虚なら（たとえば $n = n$ のような）、生まれるのは検査済みの無意味だけです。

証明の中身は読み飛ばしてよい場面でも、主張文と定義だけは人間が読む ── この一線は、AI が証明を量産する時代にこそ重みを増します。

この論点は、筆者の公開済みの別の記事 形式証明は「仕様が人間の意図を反映しているか」は保証しない ── Correctness と Appropriateness の境界で正面から論じました。

議論をまとめましょう。

sorry が残っていないかを確かめ、どんな公理に依存しているかを確かめ、主張文を読む。

前の２つは #print axioms の一行で確認できます。

以上３つを確認することで、Lean 4 のコードを一行も書けなくても、形式検証の成果物を正しく解釈できるようになります。

確認の前提 ── 審判そのものは正しいか

この３つの確認には、暗黙の前提があります。

カーネルという審判自身が、正しく作られているという前提です。

本記事の公開直前、2026年7月に、この前提を試す事件が起きました。

AI支援で作られた「コラッツ予想の反証」が Lean に受理されたのですが、調査の結果、証明はカーネルの実装の不具合（入れ子になった帰納型の検査漏れ）を突いたもので、数学的には成立していませんでした。

sorry も追加の公理も使っていない、外見上は完全な証明でした。

つまり、本節の確認１と２だけでは見抜けない種類の欠陥が、現実に作られたのです。

ただし、この事件があっても、３つの確認の価値は変わりません。

むしろこの不具合を見抜いたのは、本節で述べてきた確認の営みそのものでした。

受理された証明を鵜呑みにせず、研究者が Lean の上で内容を調査したところ、前提なしに False（偽）が証明できるという異常を突き止めたのです。

異常は小さな再現コードにまとめられて開発チームへ報告され、約１時間後には修正が作られて、同日中に修正版が公開されました。

さらにこのプロジェクトは、Lean とは別に Rust という言語で実装された独立の検査器による確認も通過していたのですが、そちらにも旧版に別の不具合があったことが判明し、あわせて強化が進んでいます。

独立の検査器の強化も進んでいます。

カーネルは信頼の終着点ではなく、それ自体が検査され続ける部品である
── 審判を疑う仕組みまで含めてが、形式検証の文化なのです。

本事案から得るべき教訓は、成果物が「どのバージョンの Lean で検査されたか」まで確かめることの大切さです。

なお、Mathlib は日々、長する動く図書館です。
ある日、定理の名前が変わることもあります。

そのため、形式化の成果物や解説記事には「どのバージョンで、いつ検査したか」を記すのが良い習慣です。

応用編 その３ ── 学習リソース

• "Theorem Proving in Lean 4" ── 公式の定理証明入門。本記事の次の一冊に最適です
   
• "Functional Programming in Lean" ── プログラミング言語としての Lean 4 の公式入門
   
• "Mathematics in Lean" ── Mathlib を使った数学の形式化の公式入門
   
• Natural Number Game ── ブラウザで遊べる証明パズル。ゲーム感覚で帰納法まで身につく、世界的な定番教材です
   
• Lean コミュニティの Zulip ── 開発者と数学者が集う公開チャット。初心者の質問チャンネルもあります

日本語の情報も、この数年で急速に充実しています。

日本語コミュニティの lean-ja（https://lean-ja.github.io/）が、Discord での交流と勉強会、そして "Theorem Proving in Lean 4" をはじめとする主要教科書の日本語訳を進めており、コード例で学べる日本語資料 Lean by Example も公開されています。

英語の壁を理由に足踏みする必要は、もうありません。

ブラウザの Lean 4 Web から先へ進みたくなったら、手元の環境は elan というバージョン管理ツールと、VS Code の Lean 4 拡張機能で作るのが標準です。

具体的な手順はこの記事には書きません。

手順は変わることがあるので、公式サイトのクイックスタートに従うのが、いちばん確実で新しい道だからです。

付録 ── 本記事に登場したタクティクは、この１０個だけ

網羅的な一覧は公式ドキュメントに譲り、本記事で実際に使った１０個だけを復習用にまとめます。入門の範囲は、この１０個で十分に歩けます。

タクティク	役割	初出
rfl	「定義どおり計算すれば両辺は同じ」で締める	基礎編 その３
rw	等式を使って式を書き換える	動かす体験
induction	帰納法で場合分けする	動かす体験
exact?	ゴールを閉じられる定理をライブラリから検索する	動かす体験
ring	環（足し算と掛け算）の等式を自動で整理する	基礎編 その４
omega	整数・自然数の線形算術を自動で判定する	業務の現場
simp	渡した等式群で式を単純化する	業務の現場
decide	有限の計算で白黒つく主張を、計算で判定する	業務の現場
norm_num	数値まわりの主張を自動で片づける	数学者の５つの型
nlinarith	非線形の不等式を、人間のヒント付きで解く	数学者の５つの型

応用編 その４ ──【対話篇】タロウくんと専任講師の対話

タロウくん
先生、AlphaProof が銀メダルなら、僕が数学を勉強する意味はもう無いんじゃないですか。

専任講師
逆に聞くけれど、AlphaProof の答案が正しいと、誰が保証したんだったかな。

タロウくん
Lean 4 のカーネル……あ、AI 自身じゃないんですね。

専任講師
そう。AI は答案を量産する側で、正しさの保証は定理証明系の側にある。

そして、その定理証明系に「何を証明させるか」
── 問題を選び、主張を型として書き、Mathlib のどの定理と結ぶかを設計する仕事は、いまも人間のものだ。

タロウくん
Mathlib って、AI が作ったんじゃなくて、人間の数学者たちが１０年かけて積み上げたものなんですよね。

専任講師
うん。

AIはその図書館で学んだ生徒であって、図書館を建てた側じゃない。

だから君が Lean 4 を学ぶことは、AI と競争することではなくて、AI が働く舞台の設計図を読めるようになることなんだ。

タロウくん
舞台の設計図が読める人になる、ですか。

・・・先生、そこでもう少し質問があります。

フェルマーの最終定理みたいな有名な定理の証明を Lean 4 でやるとき、Mathlib は実際にはどう使われるんですか？

専任講師
二役をこなすんだ。

ひとつ目の役割は、土台 ── 群も環も位相も 証明が寄りかかる基礎はぜんぶ Mathlib から呼ぶ。

もうひとつの役割は、寄贈先だ。

形式化の途中で必要になったのに Mathlib にまだ収蔵されれいなかった理論は、Mathlib側に納めながら進む。

フェルマーのプロジェクトは、数論の基礎理論を Mathlib に納品し続ける公共工事でもあるんだよ。

タロウくん
そのコードは、Web で公開されているんですか？
僕でも読んで、定理証明の仕方をコード例から学べますか。

専任講師
公開されている。

Mathlib本体も、フェルマーやリキッド・テンソルの各プロジェクトも、GitHub 上で全行を誰でも読める。

ただし、大定理のコードは登山でいえば最高峰の岩壁で、初心者の練習台には向かない。

それでも読み方はある。

応用編を思い出してごらん
── 証明の中身は追わず まず主張文と定義だけを読む。

それから、大きなプロジェクトは blueprint（ブループリント）という文書を公開していることが多い。

人間向けに書いた証明の設計書とコードの対応表みたいなものだ。

地図を blueprint で眺めて興味のある一つの峰だけ、その部分のコードを覗く。

学ぶ順番としては Natural Number Game で足慣らし、Mathematics in Lean で登山道、そして Mathlib の小さな定理 ── 岩壁は最後でいい。

タロウくん
その大定理の形式化に、数学者と証明エンジニアで数年単位の時間がかかると報じられていました。
なぜ、そんなにかかるんですか？

専任講師
理由は大きく３つある。

第１に行間だ。

紙の証明で「自明」「同様にして」と書かれた１行の裏に、形式化では数十の補題が要る。

人間の読者は行間を好意で埋めてくれるがカーネルは１ミリも埋めてくれない。

第２に前提の山だ。

定理そのものよりも、定理が寄りかかる分野の基礎全体
── 教科書で数冊ぶん ── が Mathlib に無ければ、そこから作ることになる。

だから所要時間は実のところ Mathlib の充実度の関数なんだ。

タオの PFR 予想の形式化が数週間で済んだのは、あの分野の基礎が Mathlib に揃っていたから。
フェルマーが年単位なのは、数論幾何の基礎からの大工事だからだ。

第３に定義の設計。

数学の概念を「どの形で形式化するのが正しいか」を選ぶこと自体が、研究に近い創造の仕事になる。

タロウくん
でも先生、そんなに時間がかかるなら、Lean 4 を使わずに、数学者が手計算や、Mathematica や Sage みたいな数学ソフトで検証しても、結局同じくらいの時間なのでは？

専任講師
いちばん大事な疑問だ。
答えは ── 作っているものが違う、となる。

Mathematica や Sage は計算の道具だよ。

具体的な数を入れて答えを出す。

何万個の例で確かめてもそれは「試した範囲では正しかった」であって、「すべての場合について正しい」という無限の主張には原理的に届かない。

業務の現場の節の事例４を思い出してごらん ── 有限の実験と、全数についての証明は、別の生き物だった。

では手計算と査読はどうか。

あれは人間の信頼のネットワークで支えられていて リキッド・テンソル実験が始まった動機そのものが「最前線の証明は難解すぎて、人間の査読と検証だけでは提唱者本人にも確信が持てなかった」だった。

そして最後に資産の話がある。

形式化は一度きりの検証作業じゃない。できあがったものは以後いつでも機械が再検査でき、Mathlib に納められれば世界中の次の証明の部品になる。

かかった数年は検証の費用というより、永続する数学のインフラへの投資なんだ。

タロウくん
もう一つだけ聞かせてください。

望月教授の宇宙際タイヒミュラー理論は、教授が独自に生み出した数学概念や記号で書かれていて、トップレベルの数論幾何の数学者でも、まず既存の数学の言語に翻訳する作業が必要だと聞きました。

その解読がまだ終わっていないのに、どうやって Lean 4 のコードに書き下す作業を進められるんですか？

専任講師
鋭い。

そこは順序の想定を、一つだけ裏返してほしいんだ。

「人間の翻訳が終わってから清書として形式化する」のではない。

LANA プロジェクトの発表文を読むと、チームは１年半にわたり各地で合宿を重ねて論文を精読し、論点を整理してきた。

活動の大半は、まさに君の言う人間による読解と翻訳だ。

形式化はその読解に品質検査として並走している。
形式化を念頭に置いて読むと曖昧さの残る読み方が許されなくなるからね。

足元の戦略もある ── まず土台の遠アーベル幾何学の基礎（ガロア圏や基本群）を Lean と Mathlib に整備する。

そして肝心の IUT本体について、発表によればチームは核心の一点 ── 第３論文の定理3.11から系3.12を導く論理 ── を「形式化できるほど正確に言語化できたが、その先へ進めずにいる」段階まで来ている。

それが証明のギャップなのか自分たちの理解の限界なのかは断定せず、中立の立場で望月教授との対話を続けると明言している。

タロウくん
形式化が止まった場所がそのまま、論争の核心の場所を指している ── ということですか。

専任講師
そのとおり。

人間どうしの議論では「そもそも、どこで意見が分かれているのか」自体が曖昧になりがちだった。形式化は誰の権威にも寄らず、その一点を座標として特定する。

翻訳が終わったかどうかの判定を、人間の合意ではなく機械の言葉への翻訳可能性で行う
── これがこの検証の新しさだ。結論がどちらへ転んでも、数学の進み方として意義がある。

タロウくん
話は変わりますが、もう一つ気になっていたことがあります。

TL;DR に「Lean 4 は定理証明系であると同時に、汎用のプログラミング言語でもある」とありました。

汎用ということは、定理証明のためだけでなく、一般的なソフトウェア開発とかデータ解析とか、機械学習や深層学習や Web 制作なんかにも Lean 4 は使われているんですか？

企業で Lean 4 プログラマがソフトウェア開発をしている現場も、あるんですか。

専任講師
正直に答えよう。
「汎用」には２つの意味があって、Lean 4 が満たしているのは片方だ。

まず能力としての汎用性
── Web サーバもコマンドラインツールも書ける言語仕様と、C言語を経由する効率のよいコンパイルを持っていて、現に Lean 4 のコンパイラは、その本体が Lean 4 自身で書かれた大規模ソフトウェアとして毎日動いている（実行環境の低層は C言語だ）。

ここは本物だ。

だが普及としての汎用性 ── データ解析や機械学習や Web 制作の現場で広く選ばれているか ── で言えば、答えはノーだ。

その現場には Python や JavaScript の巨大なライブラリ生態系があって、Lean 4 にはまだそれに相当する蓄積がない。

深層学習の訓練を Lean 4 でやっている企業は、まず無いと思っていい。

科学計算のライブラリを Lean 4 で作る研究的な試みは芽生えているが、実務の主役は当分 Python のままだろう。

タロウくん
じゃあ、Lean 4 を仕事で書いている人は、いないんですか。

専任講師
いや、いる。ただし職種が違うんだ。

Lean 4 を毎日書く職業は現実に生まれている ── Lean 本体とその道具立てを開発する Lean FRO のエンジニア、Amazon で Cedar のような検証プロジェクトに携わる人たち、そして AI ×数学に取り組む研究機関や企業が「Lean を書ける人」を採用し始めている。

ただ、その仕事の中身は Web 画面を作ることではなく、検証と形式化だ。

証明エンジニア という呼び名も定着しつつある。整理するとこうなる
── Lean 4 は「Python の代わり」を目指す言語ではなく、「プログラムと証明を同じ言語で書ける」ことに存在意義がある言語だ。

データ解析は今日も Python でやればいい。

ただし「ここだけは絶対に間違えられない」という部分がコードの中に現れたとき、証明ごと書ける言語を知っているかどうかが、君の武器の差になる。

タロウくん
その「武器」のところを、もう少し聞かせてください。

業務の現場の節の事例みたいに、業務の要件がある数学構造と対応していると Lean 4 で証明できたとします。

その証明って、書いて終わりですか？

それとも、その後のビジネス設計で何かの役に立つんですか？

専任講師
証明が通った瞬間に、２つのことが同時に始まるんだ。１つ目は、いいほうの話 ── その数学構造について数学者たちが積み上げてきた定理の一群が、まとめて君の武器になる。事例１を思い出してごらん。

割引の演算が「どの順でも同じ」と確認できたということは、順序や分け方を気にしなくてよい、という種類の定理たちが、君の割引システムにもそのまま当てはまるということだ。

適用順を自由に実装してよい、処理を分割して並列にしてよい、順序の組み合わせを網羅するテストは要らない ── 一つ一つ自分で確かめるはずだった保証が、構造の名前ひとつでまとめて手に入る。Mathlib は、その武器の在庫倉庫でもあるんだよ。

タロウくん
それは、いいことずくめに聞こえますが。

専任講師
だから２つ目がある
── 同じ証明が、今度は制約になるんだ。構造が確認された後は、新しい要件や新しい機能を追加するたびに「この追加は、あの構造を壊していないか」を確かめる義務が生まれる。

たとえば君の割引システムに、営業部から「合計金額から１０パーセント引くクーポンも作りたい」という新機能の要望が来たとしよう。定額の割引と割合の割引は、順序で結果が変わる ── １０００円から１００円引いて１割引けば８１０円、先に１割引いてから１００円引けば８００円だ。

「どの順でも同じ」という証明済みの柱に、この新機能は正面からぶつかる。Lean 4 に掛ければ、事例４と同じように反例を突きつけられる。

タロウくん
壊れてしまったら、どうするんですか？

専任講師
道は２つ だ。

１つ目の対応策 ── 新機能の側を直す。

割合クーポンをあきらめるか、定額に設計し直して、いまの構造を守る。

２つ目の対応策 ── モデルの側を探し直す。

「どの順でも同じ」という構造は手放し、「割引は会員、クーポンの順で必ず適用する」のような新しいルールでビジネスを表現し直す。

その上で、その新しい姿に合う数学構造を探し、証明もやり直す。

そして肝心なのはここだ。

どちらの道が正しいかを、数学も Lean 4 も教えてくれない。

顧客への見え方、会計監査への説明、システム改修の費用
── それらを天秤に掛けられるのは、そのビジネスの目的を知っている人間だけだ。

機械の仕事は「柱と増築案がぶつかっています」と正確に告げるところまで。

決めるのは、ビジネスの側に立つ君なんだよ。

タロウくん
証明はゴールじゃなくて、ビジネスの設計図に「守るべき柱」を一本立てる作業なんですね。

柱があるから、上に安心して増築できる。

でも、柱に当たる増築案が来たら、案を変えるか、柱ごと設計し直すか、決めなくちゃいけない。

専任講師
いい要約だ。

その決断の質は、柱の意味 ── つまり数学構造が何を保証し、何を保証しないか ── を分かっている人ほど高くなる。

数学構造に関して、深い学識・教養をもっているかどうかが問われる場面は、証明を書く瞬間だけじゃない。

証明の後の、この意思決定の場面なんだ。

タロウくん

あと、いちばん根本の不安を聞かせてください。
業務の現場の節の４ステップの②に、数学構造の見当を付ける場面がありましたよね。

でも、数学知識がないと「このビジネス要件を満たす数学構造は群だ、いや環だ、体だ、モノイドだ、テンソルだ、無限次元ヒルベルト空間だ、非可換環だ」なんて仮説を立てること自体が、そもそもできないですよね。

Lean 4 のコードに形式化して証明する以前に、証明すべき数学構造を思いつくことができない気がします。

専任講師
以前なら、そのとおりだった。でも、道具の状況が変わったんだ。

Claude Code、Kiro、Copilot、GitHub のコーディングエージェント ── いまは開発の道具箱の中に、数学知識の相談相手が入っている。

業務要件を貼り付けて「この要件に対応する数学構造の候補を挙げてほしい」と頼めば、エージェントはこんなふうに伴走してくれる ──「候補はモノイドです。理由は、分割集計の一致には結合律と単位元だけで足りるからです。

もしこの後『操作を必ず取り消せること』という要件が加わるなら、候補は群とその仲間に絞り込まれます」。

候補と、その理由と、要件が増えたときの絞り込み
── この対話に付き合ってくれる相棒がいる時代なんだよ。

分からない名前が出てきたら「モノイドとは何ですか」と、その場で聞き返せばいい。
君がさっき挙げた難しそうな名前の羅列に、威圧される必要はもう無い。

タロウくん
じゃあ、数学知識はもうエージェント任せでいい、ということですか？

専任講師
そこは、はっきり言っておかないといけない。

エージェントはハルシネーション ── もっともらしい嘘 ── を起こす。
存在しない定理名を挙げたり、当てはまらない構造を自信満々に勧めたりする。

だからね、役割分担はこうなる。

気づきの生産はエージェント。

気づきの妥当性の最終チェックは人間。

そして、白黒つける最終判定者は、 Lean 4だ。

応用編の検分の話と、まったく同じ構図だろう。

君の言う「数学知識がないと一歩も前に進めない」という状況は終わった。

エージェントが候補と理由と絞り込みで伴走してくれる分、仕事の生産性は上がる。

でも、「数学の教養がある人ほど、エージェントの提案の当否を早く見抜き、良い問いを返せる」という差は残る ── むしろ広がっていく。

数学教養は入場券ではなくなった代わりに、伴走の速度と質を決める装備になったんだ。

タロウくん
Lean 4 や Rocq、Agda のような定理証明系は、数学者が未解決の定理を証明したり、ZEN大学の IUT 理論の検証プロジェクトのような場面で使ったりするものだとばかり思い込んでいました。

でも先生、この記事で見てきたような使い方
── 企業の業務要件や製品要件の一部分について「対応する数学構造は何かあるだろうか」と仮説を立てて、Lean 4 で証明や反証を掛ける
── は、実際の企業事例があるんですか？

それとも、事例はまだ知られていなくて、こういう使い方もできますよという、この記事からの独自の提案なんですか？

どちらなんでしょう？

専任講師
正直に答えよう。
半分は実例があり、半分はこの記事の提案だ。

実例の側から話す。

企業が定理証明系を実務に使った事例は、確かにある。

Amazon は、認可ポリシー言語 Cedar の設計 を Lean 4 のモデルで検証しながら開発している。

さらに、ソフトウェアの現場の節で触れた seL4 や CompCert のようなシステムの正しさを丸ごと証明したプロジェクト もある。

金融や暗号の分野 でも、仕様の検証に形式手法を使う会社は実在 する。

だから、「定理証明系は数学者専用」という思い込みは、事実としてもう崩れている。

ただし、だ。

それらの事例はどれも、「ソフトウェアそのものの正しさ」を証明する使い方
── 検証の対象がコードや仕様である場合
── に集中している。

この記事がやってみせた使い方は、少し違うだろう。

割引の可換性、権限の順序、税計算の反例
── 検証の対象がコードではなく、ビジネスルールそのもの だった。

「業務要件に数学構造の仮説を立てて、証明か反証で白黒つける」という型を、このサイズの小ささで日常の設計判断に使うような事例は、私の知るかぎり、まだ一般的ではない。

だからね、タロウくんの問いへの答えはこうなる
── 部品はすべて実在する。言語も、Mathlib も、企業利用の前例も、LLM の伴走も。

しかし、それらを「業務要件の設計検証」という一点に組み合わせて、Python エンジニアの日常の道具にしようというのは、この記事の提案だ。

提案というのは、まだ誰の常識でもない、ということでもある。

逆に言えば ── いま始めた人が、最初の事例を作る側に回れるということだよ。

専任講師
道具は揃っている。あとは、君が最初の一枚のカードを書くかどうかだけだ。

タロウくん
ここまで聞くと、Lean 4 が万能に思えてきました。

逆に、数学の証明でも、ビジネス要件を数学の観点から設計する実務でも、Lean 4 が得意でない分野、原理的にできない分野って、あるんですか？

そういう分野では HOL や Isabelle や Rocq や Agda や Idris 2 を使うべきだ、みたいな言語選択の基準があれば知りたいです。

専任講師
ある。

しかも、「実装の出来が悪いから苦手」ではなく「土台の選択ゆえに、原理的にそうなる」という種類の得意不得意なんだ。

使い分けの節の表は用途で比べたから、今度は土台で比べよう。

各言語が拠って立つ論理・公理系と型システムの理論は、それぞれ違う。

強みが違うのは、その土台が違うからだ。

タロウくん
その、各言語が立脚する論理公理系や型システム理論を、表にしてもらえますか。

そして、土台と「できること・できないこと」の結びつき を、分かりやすく、でもなるべく深く教えてください。

専任講師
いいだろう。

まず表を見て、それから結びつきの仕組みを３つに分けて話す。

言語	土台の論理・公理系	型システムの系譜	土台ゆえの得意	土台ゆえの不得意
Lean 4	依存型理論（CIC 系）。古典論理と選択公理を標準の道具として採用	依存型+証明どうしを区別しない設計	現代数学の大規模形式化、Mathlib、AI との接続	HoTT 系の数学（原理的に不向き）。証明からの計算の取り出し
Rocq	CIC。土台は構成的で、古典論理は公理として追加	依存型+帰納型	証明から検証済みプログラムを抽出（CompCert）	自動化の火力では Isabelle に譲る場面
Isabelle	高階論理（HOL）。古典論理	依存型のない多相の単純型	強力な自動証明（sledgehammer）、OS カーネル seL4 級の大規模検証	「長さ n のリスト」のような値に依存する型を直接書けない
HOL Light	同じ高階論理を、極小のカーネルで	同上	浮動小数点などハードウェア検証、ケプラー予想の形式化	ライブラリ生態系の規模
Agda（Cubical 含む）	マルティン=レーフ型理論。Cubical 版は一価性が公理でなく定理になる	構成的な依存型	ホモトピー型理論（HoTT）の受け皿、型理論そのものの研究	自動化が少なく、数学ライブラリも小規模
Idris 2	量的型理論（QTT）	依存型+値の使用回数を型が数える線形性	依存型での実務プログラミング、資源やプロトコルの管理	数学ライブラリはごく小さい
F*	依存型+篩型+SMT ソルバ	効果システムつき依存型	製品に直結する検証済み低レベルコード	数学の大規模形式化
ACL2	一階論理+全域再帰関数（Lisp の計算の世界）	型システムを持たない。計算そのものが論理	CPU など産業ハードウェア検証の老舗（AMD の浮動小数点除算など）	高階の抽象数学の記述
Mizar	集合論（タルスキ=グロタンディーク集合論）	型理論ではなく集合論を直接の土台に	数学論文に近い書き味と、形式化数学の長期の蓄積	プログラム検証と自動化
TLA+	時相論理+集合論。証明よりモデル検査が主戦場	型なし（集合論ベース）	分散システムの設計検証（AWS の実務採用）	数学の定理証明

結びつきの１つ目 は、型システムは「型で言える文の範囲」を決める、ということ だ。

Isabelle の土台の高階論理には依存型が無い。

だから、「長さ n のリスト」という、値に依存する型は直接書けない（性質としては別立ての述語で書けるが、型そのものにはできない）。

不便に聞こえるだろう。

でも、引き換えに論理が単純になり、外部の自動証明器と接続しやすくなる
── sledgehammer という強力な自動化や、seL4 という OS カーネル検証の金字塔は、この単純さの配当だ。

表現力と自動化は綱引きの関係にある。

だから、

「依存型の表現力が要る仕様なら Lean 4 や Rocq や Idris 2」

「巨大な検証を自動化の火力で押し切るなら Isabelle」

という選択 になる。

２つ目は、公理系は「最初から棚に置いておく真理の在庫」を決める、ということ だ。

排中律（どんな命題も真か偽のどちらか）や選択公理を最初から棚に置く Lean 4 や Isabelle は、数学者の日常の議論をそのまま書けて速い。

その一方で、Rocq や Agda の土台は、それらを置かずに進む構成的な論理で、すべての証明が「作り方の手順」を兼ねる。

この抑制的な態度にはメリットがある
── 証明から検証済みのプログラムを機械的に取り出せるんだ。

検証済み C コンパイラ CompCert は、まさにこの配当でできている。

少し補足しよう。

構成的な論理で書いた証明には、面白い性質があるんだ。

「存在する」ことを証明するには、実物の作り方を示すしかない。
だから、証明の中には計算手順が埋まっているんだ。

そして、Rocq には、証明からその計算手順を抜き出して、実行できるプログラムに変換する機能がある。

検証済みコンパイラ CompCert は、まさにこの方法で作られたんだ。
「正しいコンパイル結果が存在する」の証明から、コンパイラ本体のプログラムを取り出したわけだ。

ところが、公理 はこの性質を壊す。

公理 とは、「作り方は示さないが、成り立つと認めてくれ」という宣言 だから、公理に頼った証明には、その部分だけ計算手順が入っていない。

棚に公理を１つ足すたびに、書ける数学の範囲は広がるが、証明から取り出せるプログラムの範囲は狭まる
── この綱引きがあるから、「証明そのものを実行可能なプログラムにしたいなら、公理を節制する Rocq の文化」という選択になる。

ちなみに Mathlib は、古典論理と選択公理 ── どちらも「作り方を示さずに存在を認める」型の公理だ ── を全面的に採用している。

つまり、Lean 4 と Mathlib の陣営は、書ける数学の広さを取り、証明からプログラムを取り出す性質のほうを譲った側なんだ。

専任講師
では、反対側を選んだ言語たちの話をしよう。

広さよりも、証明からプログラム（計算手順）を取り出す性質のほうを選び取った陣営だ。

筆頭は Rocq だ。

土台の構成的な論理を守り、公理の追加を文化として節制する。

その見返りが、さっき話した抽出機能 ── 証明を書き上げると、そこから検証済みのプログラム（計算手順）を OCaml のコードとして機械的に取り出せる能力だ。

CompCert という 検証済みのCコンパイラ が商用利用の実績を持つのは、この性質の直接の配当 だ。

数学の書庫の広さでは Mathlib に及ばない。でも「証明がそのまま製品になる」という一点では、Rocq の右に出る言語はない。

Agda は、もっと純粋主義だ。

マルティン=レーフ型理論 という 構成的な土台 を、ほとんど混ぜ物なしで貫いている。

証明とプログラムの区別が、言語の設計上ほぼ存在しない
── 書いたものすべてが証明であり、同時に計算手順 だ。

研究者たちが新しい型理論の実験場として Agda を選び続けるのは、この純度ゆえだよ。

具体的に、どこで使われているか。

主戦場は、プログラミング言語と論理学の研究の世界だ。

新しい型システムを設計したら、その性質を Agda の上で形式化して確かめる ── 世界中の大学の研究室で、Agda はそういう「理論の試作台」として回っている。

発展コラムで触れるホモトピー型理論はその代表例で、複数の等しさを扱う新しい数学の検証実験は、Cubical Agda という拡張の上で進んできた。

球面のホモトピー群のような、ホモトピー型理論でしか書けない証明の計算実験も、Agda が最初の現場 だった。

物理や自然科学への応用は、まだ研究段階 だ。

物理の理論を構成的に定式化し直す試みや、圏論を経由して量子計算の性質を検証する研究に Agda が使われることはあるが、実験データの解析に日常使いされる、という段階ではない。

企業のビジネスシーンではどうか ── 正直に言えば、Agda を製品開発の主力に据えた企業事例は、ほとんど知られていない。

産業の現場で名前を見るのは、暗号通貨のような「仕様の一行が資産の消失に直結する」分野で、プロトコルの数学的な検証に研究者が Agda を使った例などに限られる。

むしろ、 Agda の産業への貢献は、間接的な形をとる
── Agda の上で試された型理論のアイデアが、数年後に Lean 4 や Idris 2 や Haskell のような言語に輸入され、そちらが実務に届く。研究の最上流で川の水質を決めている言語、と言うのが実像に近いだろうね。

タロウくん
先生、その HoTT を Agda の上で検証できるという話なんですが、HoTT を定理証明系で使うユースケースも、やはり純粋な数学研究か、物理のような自然科学の理論研究に限られるんでしょうか。

ビジネスの現場で、複数の異なる「等しさ」を、HoTT のまなざしと数学の言葉を使うことでうまく区別できて、しかもその区別ができること自体がビジネス上の大きな価値を生む
── そんな場面や文脈で Agda の HoTT ライブラリが使われている、という事例は、2026年8月現在、知られている限りでは何かないのでしょうか。

専任講師
いい聞き方だ。

「知られている限りでは」と条件を付けたね。
その条件のとおりに、正直に答えよう。

無い、というのが答えだ。

Cubical Agda の HoTT ライブラリがビジネスの現場で使われて、複数の等しさの区別が利益を生んだ
── そう報告された商用事例を、私は知らない。

2026年8月現在、HoTT の定理証明は、数学と理論計算機科学の研究の内側にある。

ただし、だ。

「複数の等しさを区別できないせいで困っている現場」なら、君も毎日見ているはずだよ。

顧客データの統合を考えてごらん。

同じ人物が、販売システムでは会員番号で、サポートシステムではメールアドレスで、広告システムでは端末の識別子で登録されている。

この３つのレコードが「同じ顧客」だと言うとき、その「同じ」は少なくとも３種類ある
── 同一の書類で本人確認された「同じ」、メールの一致から推定した「同じ」、行動パターンから確率的に推定した「同じ」。

いまのシステムの多くは、この区別を捨てて一本の「同じ」に潰してしまう。

そして潰したことが、誤った名寄せや、監査で説明できないデータ統合として、後から請求書になって返ってくる。

HoTT の眼で見れば、これは「等しさの証拠が複数あり、証拠ごとに使える操作が違う」という、まさにあの理論が正面から扱う形をしている。

データ移行だってそうだ ── 旧システムと新システムの口座が「同じ」だと言うとき、その同一視の根拠を証拠として持ち回れたら、監査への説明は別物になる。

だから答えはこう整理できる ── 問題の形は、ビジネスの現場にすでにある。

それを HoTT の道具で解いた公開事例は、まだ無い。

この距離が埋まるかどうかは分からないし、埋まるとしても、Cubical Agda がそのまま現場に入るのではなく、HoTT で磨かれた「等しさを証拠つきで扱う」という設計思想が、もっと普通の言語やデータ基盤の設計に薄まって届く、という形だろう。

理論の言葉がそのまま現場に降りてくることは稀でも、理論のまなざしは、いつも先に届くものだからね。

タロウくん
待ってください、先生。

いまの顧客データの話は、比喩レベルの議論 ではないんですか？

本当に HoTT の数学を使って、異なる等しさをそのまま取り扱える、ということなんですか。

専任講師
鋭いね。

正直に答えると ── 半分だけ本当だ。

そして、さっきの私の話し方は、その半分の境界を曖昧にしていた。
タロウくんの指摘のとおりだから、境界線を引き直そう。

本当に成り立つ部分から話す。

HoTT の土台では、$a = b$ は真偽の命題ではなく型で、その型の項が「等しさの証拠」だ。

証拠は複数ありえて、互いに区別され、値のように持ち回すことができる。

レコード $A$ の性質をレコード $B$ に引き継ぐには、どの証拠で同一視したかを明示して輸送（transport）する ── 根拠がコードに残る仕組みが、理論の側に最初から備わっている。

ここは比喩ではなく、理論の中身そのものだ。

実際、バージョン管理のパッチ ── ある状態を別の状態と同一視する操作 ── を「等しさの証拠」として HoTT でモデル化した研究が2014年に発表されている。

ホモトピー的パッチ理論 という。

「業務上の同一視を、証拠として型で扱う」という発想自体は、研究として実在するんだ。

• "Homotopical Patch Theory"（Angiuli, Morehouse, Licata, Harper、ICFP 2014） ── バージョン管理のパッチを HoTT の等しさの証拠としてモデル化した研究。対話篇で言及

タロウくん
それ、すごい話じゃないですか。

バージョン管理 って、僕たちが毎日 git で触っている、いちばん 身近な道具 ですよね。

パッチを当てる、取り消す、順番を入れ替える
── あの日常の操作の裏に「等しさの証拠」という HoTT の最先端の数学が、そのまま形になって現れている。

高度な理論が、雲の上の話じゃなくて、プログラマが毎日お世話になっているツールに具現化された、すごく良い例 ですね。

こういう事例って、他にもあるんですか？
HoTT のユースケースとして知られているものが、何か・・・。

専任講師
興奮は分かる。

ただし最初に一つだけ正確を期しておくと、あの研究はパッチ理論を HoTT でモデル化して性質を検証したものであって、君が毎日使っている git そのものが HoTT で作られているわけではない
── 理論が道具を照らした例であって、道具が理論で置き換わった例ではないんだ。その区別を守ったうえで、他の事例を挙げよう。

一番の大物は、数学それ自体の検証だ。

発展コラムで触れる 「球面のホモトピー群」のような、ホモトピー論の定理を Cubical Agda の上で形式化して、証明を機械検査つきで計算する研究が積み重なっている。

人間の手計算では何十ページにもなる繊細な議論を、機械が一行ずつ検査する
── HoTT が生まれた本籍地での、いちばん確実な使い道だ。

もう一つは、プログラミング言語の設計への影響 だ。

HoTT の研究から生まれた「一価性」の考え方 ── 同じ振る舞いをする構造は取り替えてよい、という原理 ── は、ライブラリの実装を差し替えても検証済みの性質が引き継がれる、という実務の願いと同じ形をしている。

この発想を薄めて取り込んだ言語機能や検証手法の研究が続いていて、さっき話した「川の水質」の典型例になっている。

正直に言えば、ユースケースの一覧はまだ短い。

パッチ理論、数学の検証、言語設計への影響
── 現時点で確かなのは、この３つの系統だ。

だが思い出してほしい。

可換だの結合律だのという地味な代数が、割引システムの検証に届くまでにも、百年の時間が掛かっている。

等しさの数学が git の隣まで来ているという事実は、その時間の物差しで見れば、むしろ早いくらいなんだよ。

さて、話を元に戻そう。
次に、成り立たない部分だ。

HoTT の数学を使って、異なる等しさをそのまま取り扱える、ということは半分は成り立つが、半分は成り立たない、と言ったのを覚えているかい？

ここまでは、成り立つ場合について説明してきた。ここからは、成り立たない場合を話すよ。

さっきの顧客データの話のうち、根拠つきの同一視を証拠として型で扱う、というところまでは理論に乗る
── そう言った。

だが、私が挙げた例の中には、理論に乗らないものが混ざっていた。

さっき私は「行動パターンから確率的に推定した同じ」と言ったが、あれは撤回する
── 確率的な名寄せ、「たぶん同じ顧客」は、この枠には乗らない。

等しさの証拠は論理の構成物であって、80パーセントの確度、を表す装置ではないからだ。

それから、「証拠ごとに使える操作が違う」という言い方も正確ではなかった。

理論が保証するのは、こういうことだ
── レコード $A$ とレコード $B$ が等しいという証拠が１つあれば、$A$ について成り立っていた事実（購入履歴でも、ポイント残高でも）を、その証拠を根拠にして $B$ の事実として引き継ぐことができる。

これが 輸送（transport） で、どの証拠を使っても、この引き継ぎの操作そのものは同じように働く。

理論が面倒を見てくれるのは、ここまでだ。

「本人確認の証拠のときだけ口座統合を許し、メール一致の推定ではポイント参照までしか許さない」といった業務規則 ── 証拠の種類ごとの扱いの差 ── は、HoTT が与えてくれるのではなく、設計者が型の設計で作り込むものだ。

だから正確な答えはこうなる。

根拠のはっきりした同一視を、根拠ごと型で管理する。

この部分は、HoTT の数学がそのまま扱える。

確率つきの推定や、証拠に応じた業務ルールは、理論の外で人間が設計する部分だ。

理論に載る部分と載らない部分の線を引けること ── それ自体が、この記事で何度も話してきた検分の技術だよ。

さて、Agdaについての解説は、ここで終わりにしよう。

次は、Idris 2だ。

Idris 2 は、Agda と 同じ思想 ── 書いたものが証明であり、同時に計算手順でもある、という構成的な考え方 ── を、「実務のプログラミング言語」の側へ倒した設計 だ。

依存型で仕様を型に書き込みながら、普通のアプリケーションを書くことを最初から目標にしている。

証明のための言語というより、「型で正しさを語れるプログラミング言語」
── 取り出すまでもなく、書いたものが最初からプログラムなんだ。

並べてみると、はっきりするだろう。

同じ「構成的」の側にも、証明から製品を取り出す Rocq、証明と計算の一致を貫く Agda、最初からプログラムとして書く Idris 2 という濃淡がある。

そして Lean 4 と Mathlib は、その全員と反対の岸 ── 広さの岸 ── に立った。

どちらの岸も、間違いではない。何を作りたいかが、立つ岸を決めるんだ。

３つ目は、いちばん深い分岐 ── 「証明とは何か」を問う哲学 だ。

Lean 4 のカーネルは、「同じ命題の２つの証明は区別しない」という設計を土台に焼き込んでいる。
軽くて速く、ふつうの数学の慣習にも合う。

ところが、ホモトピー型理論（HoTT）という新しい数学は、まさにその「証明どうしの違い」や「等しさの等しさ」を幾何学の構造として研究する分野なんだ。

カーネルに焼き込まれた哲学は、後から設定では変えられない。

だから、HoTT をやりたければ、一価性が公理ではなく定理として成り立つ Cubical Agda のような土台を選ぶことになる ── これが「原理的にできない」という言葉の正確な中身だよ。

表の下３つは、視野を広げるために足した顔ぶれだ。

ACL2 は型システムを持たない
── Lisp の計算そのものを論理にするという土台の選択で、AMD の浮動小数点除算の検証のような工業実績を積んできた老舗で、「型が無くても土台しだいで戦える」ことの生き証人だ。

Mizar は、型理論ではなく集合論を直接の土台に選んだ道 で、数学論文に近い書き味の形式化を何十年も蓄積してきた。

そして TLA+ は、そもそも定理証明系ですらない
── モデル検査 という 「あり得る状態を機械が総当たりで調べる」別方式が主戦場 で、時相論理という「時間の流れの中での正しさ」を語る論理を土台に、AWS が分散システムの設計検証に実務採用している。

君のビジネスの悩みが「分散処理の設計が正しいか」なら、最初に手に取るべきは Lean 4 ではなく TLA+ かもしれない。

Cubical Agda が HoTT の受け皿として表に座っているのも含めて
── 土台の数だけ、言語の生き方がある。それがこの表の読み方 だよ。

タロウくん
調べていたら、Cryptol、Whiley、Dafny、ATS、PVS、Metamath という名前も見つけました。
これらは、どういう立ち位置なんですか。

専任講師
よく見つけてきたね。

どれも設計の軸を１つずつ教えてくれる顔ぶれだから、補遺の表にして渡そう。

言語	土台	得意	不得意
Dafny	ホーア論理（事前条件・事後条件・不変条件）+SMT	普通のプログラマに近い書き味での関数・クラス単位の検証。産業採用の実績（Amazon の暗号系ライブラリ、分散システム検証の研究など）	数学の定理の蓄積
Cryptol	暗号仕様の関数型記述。実装との等価性検証は相棒ツール SAW+SMT が担う	暗号アルゴリズムの仕様を書き、C や機械語の実装が仕様どおりかを検証（AWS の暗号ライブラリ検証などで実績）	暗号以外の領域ぜんぶ
PVS	古典の高階論理+述語サブタイプ（条件つきの型）	航空宇宙の検証（NASA での長年の採用）	フルの依存型の表現力、モダンな生態系
ATS	依存型+線形型を、C 並みの性能の低レベル言語に	メモリ安全・資源安全を証明ごと書くシステムプログラミング	学習曲線が急で、コミュニティが小さい
Whiley	事前・事後条件と篩型を最初から言語に組込み+SMT	検証組込みの命令型言語という設計の研究・教育	生態系と実務採用の規模
Metamath	論理すら組み込まない、置換規則だけの極小検査器。公理系（集合論など）はデータとして与える	検証器を数百行で書ける究極の信頼性。数万件の定理データベースは AI の証明研究の教材にもなった	自動化や抽象化の支援がほぼ無く、人間が書くには忍耐が要る

この６つから学べる設計の軸を言っておこう。Dafny と Whiley は「検証を、普通のプログラマの書き味に近づける」という民主化の軸。Cryptol は「対象領域を暗号ただ一つに絞る」という特化の軸 ── まさに DSL の生き方だ。

ATS は「性能と証明の両立」、
PVS は「一つの産業（航空宇宙）で数十年鍛え続ける」という軸。

そして Metamath は思想の極北だ
── 検査器が小さいほど、検査器そのものを疑わずに済む。

本編で話したカーネルという設計思想を、極限まで煮詰めた姿だよ。

実務との距離でいえば、企業ビジネスと距離が近いのは Dafny と Cryptol、
思想を学ぶなら Metamath
── これで言語設計の見取り図が、ひととおり一周したことになる。

タロウくん
用途の違いの奥に、土台の理論の違いがあって、しかもどの土台にもトレードオフがある
── だから最強の１言語は原理的に存在しなくて、こんなにたくさんのプログラミング言語が開発されてきたんですね。

新しい言語を作るときの動機や目的も、ここから考えられそうです。

「既存の土台のトレードオフでは守れないものを守るために、土台ごと選び直す」というか。

このあたりって、型システム論とかプログラミング言語設計論とかを学べば、知見が深まりますか。
言語を設計するという仕事についても、理解を深めたいんです。

専任講師
深まる。

まさにその２つが該当分野で、学問としてはプログラミング言語理論と呼ばれる領域だ。

型システム論の世界的な定番教科書は "Types and Programming Languages"（通称 TAPL）で、日本語なら『プログラミング言語の基礎概念』のような教科書から入れる。

そして君の言い直しは、そのまま言語設計の動機の定義になっている。

Idris 2 は、「資源の使用回数を型で守りたい」から量的型理論を土台に選び、
F* は、「証明の筋肉労働を自動化したい」から SMT ソルバを土台に組み込み、
Lean 4 は、「数学の全体とメタプログラミングを一つの言語で」という目的から自己記述の依存型言語として設計された。

土台の選択こそが言語設計の核心なんだ。

仕事としても、汎用言語のコアチームは世界でも少数だが、ドメイン特化言語（DSL）
── 設定記述、API 定義、業務ルールの記述言語 ── の設計なら、普通のエンジニアの実務の中にいくらでもある。

今日やった「土台とトレードオフで言語を比べる」という見方自体が、言語設計論の最初の一歩だよ。

タロウくん
今日はたくさん質問してしまいました。

入り口ではエージェントが伴走してくれて、出口の意思決定は人間が引き受ける。

そして道具の選択の奥には、土台の理論がある
── この世界の歩き方の実感が湧きました。

先生、まずは Natural Number Game、今夜やってみます。

専任講師
いい返事だ。ゲームで帰納法に慣れたら、次は Rocq の世界も覗いてみるといい。同じ景色が、別の窓から見えるから。

対話篇で辿り着いた「言語の得意不得意は、土台の論理と型理論の選択で決まる」という見方は、それ自体を主題にした拙記事群があります。

２１の論理体系を本記事と同じ対話篇の形式で巡るif 文も SQL も、実は別々の「論理」だった ── 古典論理から量子論理まで、２１の論理体系を５人で議論【対話篇】、「論理は複数ある」という事実そのものを地図にした論理はひとつではない ── 圏論論理学がつなぐ量子論理・トポス・圏論的量子力学、そして「器（数学の宇宙）を選ぶと、なぜ古典論理か直観主義論理が決まるのか」を数学の仕組みまで掘り下げたトポスと論理の関係です。

本記事の対話篇が言語の側から登った山を、これらは論理の側から登っています。

発展コラム ──「複数の等しさ」の数学は、何の役に立つのか

対話篇で「Lean 4 と原理的に相性が悪い数学」として名前だけ登場したホモトピー型理論（HoTT）について、一歩だけ踏み込むコラムです。発展的な内容なので折りたたんであります。興味のある方だけお開きください。

コラム本文:互いに異なる「複数の等しさ」とは何か（クリックで開閉）

「等しい」に、種類がある

ふつうの数学では「a = b は、成り立つか成り立たないか」だけを問います。HoTT の出発点はその一歩先です ── 等しいとして、どの等しさか。具体例を３つ見てください。

例１（対応の選び方）── ３人の生徒 {太郎, 花子, 次郎} と３つの席 {A, B, C} は「同じ数」です。
でも、同じ数だと確かめる方法 ── 誰をどの席に対応させるか ── は６通りあります。
「等しい」という一つの事実の内側に、６つの互いに異なる等しさが入っているのです。

座席表が変われば現実が変わるように、どの等しさかには固有の情報があります。

例２（重ね方の違い）── 正三角形を持ち上げて、自分自身にぴったり重ねる方法は１つではありません。
そのまま戻す、１２０度回す、２４０度回す。「同じ形」という一言の内側に、複数の重ね方=複数の自己同一視が畳み込まれています。

この「等しさたちの集まり」こそ、数学で対称性と呼ばれるものの正体です。

例３（プログラムの表現替え）── 連結リストと配列は、どちらも「同じ列」を表せます。
同じであることの中身は、相互に変換する２つの関数の組です。
変換の組の選び方が違えば、それは別の等しさ ── データ移行の現場で書くマッピング表が、まさに「等しさの中身」にあたります。

HoTT は、この直観を土台に据えた数学です。

「a = b」を a から b への道と読み、道が複数ありうること、さらに道と道のあいだの道（等しさどうしの等しさ）まで正式な研究対象にします。

ホモトピーという幾何学の名前が付いているのはこのためです。

そして一価性（univalence〈ユニバレンス〉）という原理が「構造を保つ一対一の対応」と「等しさ」を公式に結びつけ、等しさの種類を数えることを数学として正当化します。

数学研究でのユースケース

この分野を推進したのはフィールズ賞受賞者のウラジーミル・ヴォエヴォドスキーで、動機の一つは「自分の論文の誤りに長年気づけなかった。機械に検査させたい」という切実なものでした。研究での使いどころは３つあります。

第一に、数学の基礎の新しい土台の候補（集合論に代わる出発点）。第二に、同型なもののあいだで定理を自動で移送できること ── 数学者が日常的に行う「同型だから同一視する」という省略を、原理のレベルで正当化し機械化します。

第三に、空間そのものを型として直接扱う新しいスタイルのホモトピー論 ── 球面のホモトピー群の計算のような結果が、実際に形式化されています。実装の受け皿は、対話篇で触れた Cubical Agda のほか、Rocq 上の HoTT ライブラリなどです。

産業・実務でのユースケース

正直に言えば、HoTT が製品開発の現場で広く使われている段階では、まだありません。ただし芽は具体的です。

第一に、表現の差し替えの正当化 ──「同値な型は交換してよい」という一価性の発想は、プログラムの内部表現を効率のよいものへ差し替えても外から見た性質が保たれる、という表現独立性の保証に直結します。

第二に、スキーマ移行と双方向変換 ── 旧データベースと新データベースが「同値」であることの中身（どの対応で移すか）は移行スクリプトそのものであり、等しさを一級のデータとして扱う HoTT の発想と深く響き合います。

第三に、バージョン管理の数学 ── パッチやマージを「状態のあいだの道」、マージの整合性を「道どうしの関係」として定式化する研究（パッチ理論）があり、分岐と統合の正しさを語る新しい語彙になりつつあります。

なぜ Lean 4 では、原理的にできないのか

対話篇で「Lean 4 と HoTT は原理的に相性が悪い」と述べました。ここまでの言葉が揃ったので、その理由を種明かしします。

Lean 4 のカーネルには、プルーフ・イレレバンス（proof irrelevance、証明の無差別）という設計が焼き込まれています。同じ命題に対する証明は、何通りの書き方があってもすべて同一のものとして扱う、という規則です。

とくに「a = b」という等しさの命題では、その証明はどれも同じと見なされます ── 等しさの証明は高々１通り、という性質で、UIP（uniqueness of identity proofs）と呼ばれます。

旅にたとえるなら、Lean 4 の世界の記録簿には「東京に着いたか、着いていないか」だけが残り、どの経路で着いたかは書き込まれません。経路の違いは、カーネルの規則によって最初から消される設計なのです。念のために言えば、これは手抜きではなく利点です。

違いを保存しない分だけカーネルは小さく軽く速くなり、「等しさは１種類で足りる」ふつうの数学には最適の選択です。Mathlib の巨大な蓄積は、この身軽さの上に建っています。

一方、ここまで見てきたとおり、HoTT の心臓は正反対の場所にあります。

「a = b」の証明を a から b への道と読み、３人の生徒と３つの席の対応が６通りあるように、異なる道は異なるものとして数える。

一価性とは、まさに「対応の数だけ、互いに異なる等しさが存在する」ことを保証する原理でした。

衝突は、もう見えていると思います。

カーネルが「等しさの証明はどれも同じ（高々１つ）」と決めている世界へ、「この２つの型のあいだには６通りの、互いに異なる等しさがある」と主張する一価性を公理として持ち込むと、１つしかないはずのものが６つある、という矛盾がその場で生じます。

つまり Lean 4 において一価性は「まだ証明されていない」のではなく、追加した瞬間に体系ごと壊れるのです ── これが「原理的にできない」の正確な中身です。

しかもこの規則は、設定ファイルやライブラリの層ではなく、カーネルの型検査の規則そのものに焼き込まれているため、後から変えられません。

経路を記録簿から消す駅では、経路の学問は営めない
── だから HoTT の研究者たちは、道の違いを最初から保存する Cubical Agda のような別の土台を選ぶのです。

まとめると、「等しさは１種類」という前提の上に建つのが従来の数学と Lean 4 で、「等しさの多様性」ごと扱うのが HoTT と Cubical Agda です。

対話篇で見た土台の分岐の意味を、ここまで開くとこう言えるのです。

なお、この「複数の等しさ」の数学については、独立した連載を既に開始しています。

連載初回:「型」を「空間」として捉え、「２点を結ぶ経路」の数だけ「異なる等しさ」を認識するホモトピー型理論（HoTT）は、数学と情報科学でどう威力を発揮するか?では本コラムの内容を学部数学の言葉で本格的に展開し、連載第２回:「複数の等しさ」を扱う２つの流派では、Lean 4 で HoTT が原理的にできない理由（証明どうしを区別しない設計と一価性の非両立）も、正面から解説しています。

まとめ

まとめの箇条書きに入る前に、一つだけ釘を刺させてください。Lean 4 は、万能ではありません。証明したい性質を数学の言葉で表現できなければ、Lean 4 は何一つ証明できません。

だから本当に重要なのは、「Lean を書く技術」よりも「どんな数学構造で業務を表現するか」です。

Lean 4 はその正しさを検査する機械であり、何を証明すべきかを決めるのは、最初から最後まで人間なのです ── この一線は、篩型の F* を紹介した記事でも、λProlog の連載でも、Correctness の記事でも繰り返してきた、本連載の背骨です。

• Lean 4 は、定理証明系と汎用プログラミング言語が一つになった言語であり、コンパイラから証明の道具まで自分自身で書かれた、徹底した自己記述の設計を持ちます
   
• Mathlib という数百人が育てる巨大な形式化数学ライブラリが、数学者の共同事業と AI の学習・検証の共通の土台になっています
   
• 数学の現場ではリキッド・テンソル実験、タオの形式化、フェルマーの最終定理プロジェクトが、AI の現場では AlphaProof をはじめとする証明 AI が、それぞれ Lean 4 を舞台に進んでいます
   
• ソフトウェアの現場でも、Amazon の Cedar のような検証駆動の実例が育ちつつあります
   
• 「検査済み」を受け取る側の検分点は３つ ── sorry を数え、公理を数え、主張文を読む。主張文の検分は、AI の時代にも人間の仕事です
   
• Rocq・Isabelle・Agda・F* とは目的で使い分けます。数学の形式化と AI の潮流に乗るなら、入口は Lean 4 が第一候補です

関連記事

• λProlog とは何か ── AI が数学を証明する時代、定理証明系 Rocq の内側で働く知られざる言語
   
• F*（F Star）とは何か ── Firefox・Linux・WireGuard で動く「証明済みコード」を書けるプログラミング言語の早わかり
   
• 形式証明は「仕様が人間の意図を反映しているか」は保証しない ── Correctness と Appropriateness の境界
   
• if 文も SQL も、実は別々の「論理」だった ── 古典論理から量子論理まで、２１の論理体系を５人で議論【対話篇】 ── 対話篇で触れた「土台の論理はひとつではない」を、２１の体系で一望します
   
• 論理はひとつではない ── 圏論論理学がつなぐ量子論理・トポス・圏論的量子力学 ── その出発点となった地図です
   
• トポスと論理の関係 ── ひとつのトポス（数学の宇宙）を選ぶと、なぜ古典論理か直観主義論理が決まるのか ── そして、トポス以外の「器」たち ── 古典と直観主義の分かれ目を、数学の仕組みから説明します
   
• 【連載初回】「型」を「空間」として捉え、「２点を結ぶ経路」の数だけ「異なる等しさ」を認識するホモトピー型理論（HoTT）は、数学と情報科学でどう威力を発揮するか? ── 発展コラムの主題を本格的に扱う連載の初回です
   
• 【連載第２回】「複数の等しさ」を扱う２つの流派 ── ホモトピー型理論（HoTT）と ∞-圏論のあいだに双方向の橋が開通する日はくるか? ── Lean 4 で HoTT ができない理由も正面から解説しています

出典

• OpenAI and Google outdo the mathletes, but not each other（TechCrunch、2025年７月） ── 2025年 IMO での Gemini Deep Think の公式金メダル水準と、OpenAI の自社評価の経緯

• "DeepSeek-Prover-V2"（arXiv:2504.21801） ── Lean 4 向けのオープンソース証明モデルの代表例

• "Seed-Prover"（arXiv:2507.23726） ── 形式検証を訓練の報酬に使う狙いを明記した ByteDance の論文

• Lean 公式サイト ── https://lean-lang.org/
   

• Lean 4 GitHub ── https://github.com/leanprover/lean4
   

• Mathlib GitHub ── https://github.com/leanprover-community/mathlib4
   

• Google DeepMind によるAlphaProof の発表（2024年） ── https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
   

• Cedar（Amazon の認可ポリシー言語）の GitHub ── https://github.com/cedar-policy/cedar
   

• ZEN 数学センター「LANA プロジェクト発表にあたって」（2026年３月３１日） ── https://zen.ac.jp/zmc/topics/jwz-o8xr3v6f
   

• AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明（GIGAZINE、2026年8月） ── 確認の前提（カーネル自身の正しさ）を論じた節で参照
   

• "Postmortem for Kernel Soundness Bug #14576"（Leonardo de Moura、2026年8月） ── 開発者本人による経緯の一次情報