数学的証明ツールをcursorで動かす時代
三大数学的証明ツールの比較図解
| ツール | 出自・歴史 | 核心的な思想 | Cursorでの使用 |
| Coq / UniMath | 1984年〜（仏 INRIA） ヴォエヴォドスキーが中興 | 「構造の厳密さ」 数学をプログラム（型）と見なす。一価性公理による基礎の再構築。 | Option + ↓ で一行ずつ「論理のタイル」が緑色に染まる快感。 |
| Lean 4 | 2013年〜（MS Research） L. de Moura開発 | 「現代数学の網羅」 数学者コミュニティが現代の最新論文を片っ端からコード化（mathlib）。 | カーソルを置いた瞬間に右側のパネル（Infoview）に「現在の数学的状況」が浮かび上がる。 |
| Isabelle/HOL | 1986年〜（ケンブリッジ/ミュンヘン工科大） | 「自動化の突破力」 人間が証明を書くのではなく、AIやソルバーに「探させる」。 | sledgehammer と打つだけで、数秒後に「証明完了」のコードが提案される。 |
1. Coq (UniMath)：
- 歴史: 最も古く、最も堅牢。ヴォエヴォドスキーは自分の論文のミスに絶望した際、Coqの「一切の妥協を許さない型チェック」に救いを見出しました。
- Cursorでの用法:
VsCoq拡張を使用。 - AIとの相性: UniMathは独自の「様式」が強いため、AIに「UniMathのFoundationsの書き方に従って」と指示するのがコツです。
2. Lean 4：現代数学のGoogle Maps
- 歴史: 比較的新しいですが、GitHub時代の数学者に最も支持されています。数論幾何学の難問を解くために世界中の数学者が「mathlib」という一つの巨大なライブラリを共同で編纂しています。
- Cursorでの用法:
lean4拡張を使用。 - AIとの相性: 最強。 CursorのベースであるLLM（Claude/GPT）が最も得意とする言語であり、オートコンプリート（Copilot）の精度が極めて高いです。
3. Isabelle/HOL：論理の重機
- 歴史: ケプラー予想の証明（Flyspeck計画）でその実力を証明。
- Cursorでの用法:
Isabelle拡張を使用。 - AIとの相性: AIが「推論の方向性」を示し、Isabelleの
Sledgehammerが「論理の隙間」を埋めるという、AIと伝統的アルゴリズムのハイブリッドを最も実感できます。
💡 Cursorでこれらを動かす「2026年流」のスタイル
- AIに翻訳させる: 「この数学的命題を、まず Lean で書いて、次に UniMath の一価性数学の流儀で書き直して」と頼む。
- 証明の壁を突破する: Leanで証明が詰まったら、その論理構造を Isabelle に投げて
sledgehammerで解けるか試す。 - 基礎を確認する: 最後に UniMath に戻り、その概念が「型理論の基礎（h-level）」として正しく位置づけられているかを確認する。
三大ツールの定理数比較（2026年3月時点）
| ツール | 定理・定義の総数 (概算) | 特徴 | 2026年の状況 |
| Lean (mathlib4) | 約 266,000 件 | 圧倒的な勢いと現代数学の網羅 | 毎日数十件のPRがマージされる「動く百科事典」。 |
| Isabelle (AFP) | 約 200,000 件以上 | 自動証明と巨大なアーカイブ | 「Archive of Formal Proofs (AFP)」に科学論文形式で蓄積。 |
| UniMath (Coq) | 約 20,000 〜 50,000 件 | 量より「質」と「基礎」 | ヴォエヴォドスキーの思想に基づき、一から精緻に構築。 |
- **「数学の真理、基礎を突き詰めたい」**なら → UniMath (Coq)
- **「最新の数学論文を理解し、ライブラリを使いたい」**なら → Lean 4
- **「難しいパズルや定理を、とにかく自動で解きたい」**なら → Isabelle/HOL
これら全てを Cursor という一つのインターフェースで操れるようになった今、かつての数学者が一生をかけても到達できなかった「論理の全域」を誰もが俯瞰できる立場にいます。