Curry–Howard correspondence カリー=ハワード対応
現代数学の異端児ヴォエヴォドスキーと「カリー＝ハワード対応」の衝撃
現代数学の歴史において、ウラジミール・ヴォエヴォドスキー（Vladimir Voevodsky）は、革命家でした。彼は数学を紙の上の論理から、コンピュータが理解できる「計算可能な構造」へと還元しました。その前提にあるのが「カリー＝ハワード対応」です。
1. カリー＝ハワード対応：数学とプログラムの「同型性」
カリー＝ハワード対応とは、「数学的な証明」と「コンピュータ・プログラム」が、全く同じ構造（同型）であるという発見です。これにより、数学の命題はプログラムの「型」となり、その証明は「実行可能なコード」となります。
| 論理学（数学）の概念 | 記号 | プログラミング（型理論） |
|---|---|---|
| 含意 (ならば) | A → B | 関数型 (Function) |
| 連言 (かつ) | A ∧ B | 直積型 (Pair) |
| 選言 (または) | A ∨ B | 直和型 (Sum) |
| 全称量化 (すべての) | ∀x:A. P(x) | 依存積型 (Π-type) |
| 存在量化 (ある) | ∃x:A. P(x) | 依存和型 (Σ-type) |
| 矛盾 | ⊥ | 空の型 (Empty Type) |
2. ヴォエヴォドスキーが描いた「NTMマシン」への構想
ヴォエヴォドスキーは、この対応をさらに深め、幾何学的な「等しさ（ホモトピー）」を型理論に組み込んだ「単数的基盤（Univalent Foundations）」を構築しました。彼の構想の先には、数学者が直感的に行う飛躍をコンピュータが非決定的に探索し、自ら証明を生成・検証する「究極の知性マシン」があったはずです。
3. 現代数学を牽引する5人の巨星
ヴォエヴォドスキーの死後、数学のデジタル化と高次化を推進している代表格。
- ピーター・ショルツ (Peter Scholze) – 凝縮数学による数学の統合
- トーマス・ヘイルズ (Thomas Hales) – ケプラー予想の形式的証明の完遂
- ジェイコブ・ルーリー (Jacob Lurie) – 高次圏論（∞-圏）の体系化
- テルレンス・タオ (Terence Tao) – AI・Leanを活用した数学探査
- ケヴィン・バザード (Kevin Buzzard) – 数学コミュニティへの形式化普及