セミナー「コンピュータと数学」紹介 [20240831]

全体概要

本セミナー「コンピュータと数学 ─ TuringからVoevodksyまで」は、マルレク連続講座の第一回として、コンピュータと数学という二つの営みが交差してきた知的歴史を辿りながら、生成AIの次の地平を展望する試みです [p.1], [p.2]。

その根底にある中心的な「問い」は、1950年にAlan Turingが提起した「機械は考えることができるか？」という命題にまで遡ります [p.18]。Turingはこの問いが当時「異端」とみなされることを自覚しながらも、「今世紀の終わりには人々の意見が大きく変化する」と予言しました。その予言は、生成AIの登場から75年後の現在、急激な形で現実となりました [p.20], [p.21]。

セミナーが強調するのは、こうした変化の評価にあたって「AI」という言葉では捉えきれない視点、すなわち「コンピュータは、それ自身が数学的＝論理的能力を持つ」という考え方の重要性です [p.10], [p.24]。この立場から見れば、大規模言語モデルの上に数学的能力を構築しようとするアプローチは、コンピュータが本来持つ力を迂回する回り道に過ぎないとも言えます。

この「計算＝証明＝プログラム」という認識は、1930年代のGödel、Church、Turingによる「計算可能性」の研究に端を発し [p.25], [p.26]、1960〜70年代のCurry-Howard対応を経て [p.58]〜[p.93]、Martin-LöfのDependent Type Theory [p.99]〜[p.130]、そしてVladimir VoevodskyのHomotopy Type Theory（HoTT）とUnivalent Foundationsへと結晶化されました [p.132]〜[p.198]。

Voevodskyは「すべての数学的証明はコンピュータ・プログラムの形をとるべきだ」と主張し、UniMathプロジェクトとして実践しました [p.37]〜[p.42]〜[p.47]。彼の2017年の早すぎる死は壮大な計画を中断させましたが、そのビジョンは後継者たちによって継承され、Lean上のmathlibや2024年のSchool on Univalent Mathematics等の形で広がりを見せています [p.48]〜[p.52]。最後のPart 3では、連続体仮説・Feit-Thompson定理・ケプラー予想という三大事例を通じて、コンピュータによる数学的証明が現実のものとなっていることが示されます [p.201]〜[p.259]。

講義のロードマップ

■ Part 1: 機械は考えることができるか？

• この部の核心:

TuringとVoevodskyという二人の巨人を軸に、「機械の思考」をめぐる人類の認識変化を俯瞰します。Turingの1950年論文が提起した問いが75年かけて現実となった経緯を辿りつつ、セミナー全体の問題意識─コンピュータはそれ自体で数学的・論理的能力を本来的に持っているという視点─を確立します [p.3]〜[p.15]。Voevodskyは数学における「誤りの蓄積」という危機を直視し、コンピュータによる証明検証という革命的解決策を提唱した数学者として紹介されます [p.34]〜[p.47]。

• 論理展開:
• Turingの論文"Computing Machinery and Intelligence"(1950)の問いと予言、および75年後の急激な変化の現実 [p.18]〜[p.22]
• 「AIを主語」にするのではなく「コンピュータを主語」にすることの意義、三つのビジョン（言語と論理の統合・LLM延長の限界・コンピュータ固有の論理能力）[p.8]〜[p.12]
• VoevodskyのフィールズMath受賞と自身の誤証明体験、UniMathプロジェクトの立ち上げ [p.29]〜[p.47]
• mathlibとの連続性、2024年Minneapolis Schoolによるビジョンの継承 [p.48]〜[p.52]

■ Part 2: 「計算＝証明＝プログラム」という認識の発展

• この部の核心:

1930年代の計算可能性研究から出発し、Curry-Howard対応、Martin-LöfのDependent Type Theory、VoevodskyのHomotopy Type Theory（HoTT）に至る「型の理論」の発展史を丁寧に辿ります。「命題は型であり、証明は項である」という洞察が、コンピュータを数学的証明の担い手として位置づける理論的基盤であることを明らかにします [p.55]〜[p.198]。

• 論理展開:
• Curry-Howard対応: GödelとChurchとTuringの計算可能性理論の同値性 [p.25], [p.26]。Curryの1934年の発見（型付きラムダ計算と直観主義論理の対応）[p.62]〜[p.68]、KolmogorovのBHK解釈 [p.70]〜[p.72]、HowardのPropositions-as-Types [p.74]〜[p.93]、`a:A`の多様な解釈（集合・問題・命題・型・空間）[p.95]〜[p.97]
• Martin-LöfのDependent Type Theory: Dependent Type（従属型）の導入 [p.104]〜[p.107]、Identity Type（同一性型）[p.102]、判断(Judgement)と命題の区別、`Γ ⊢ a:A`という形式体系 [p.108]〜[p.130]
• Homotopy Type Theory I（Dependent Type）: 型を「空間」、項を「点」として解釈するVoevodskyの視点 [p.133]〜[p.134]。Dependent TypeをB上のfibrationとして捉えるGrothendieck construction [p.137]〜[p.155]、Tai-Danaeのcopresheaf意味論との接続 [p.155]〜[p.157]
• Homotopy Type Theory II（Univalent Foundations）: パスによる同一性解釈・homotopy・contractibility [p.161]〜[p.173]。Univalence Axiomの発見─「同一性と等価性の等価」─と構造主義の原理の帰結 [p.178]〜[p.198]

■ Part 3: コンピュータによる証明

• この部の核心:

型の理論が生み出した証明支援システム（Lean、Coq、HOL Light等）を使って、20世紀数学の難問が実際にコンピュータで「証明」された三つの事例を紹介します。「証明はプログラムである」というビジョンの現実化を、具体的なGitHubリポジトリへの言及も交えて実感的に提示します [p.201]〜[p.259]。

• 論理展開:
• 連続体仮説の独立性: Cantor→Hilbert→Gödel→Cohenの400年史 [p.203]〜[p.215]。Jesse Michael HanらによるLean上での形式的独立性証明(2020)とflypitchリポジトリ [p.219]〜[p.226]
• Feit-Thompson定理の形式的証明: Georges Gonthierによる四色問題(2004)・奇数位数定理(2012)のCoq証明。15,000定義・4,300定理・17万行のソースコード、6年間のチーム作業 [p.227]〜[p.245]
• ケプラー予想の証明: 1611年ケプラーの予想からHales(1998年の査読留保)、Flyspeckプロジェクト(2003〜2014)、arXiv論文(2015)・学会受理(2017)へ [p.246]〜[p.256]。Perelman/ポアンカレ予想の事例との対比─コンピュータ検証のない証明が抱える「信頼の問題」[p.257]〜[p.259]