エレファントな証明――四色定理、計算機の泥沼、そしてAI時代の数学的真理 #四色定理 #AI時代の数学者 #形式検証 #科学社会学 #十16
エレファントな証明――四色定理、計算機の泥沼、そしてAI時代の数学的真理 #四色定理 #AI時代の数学者 #形式検証 #科学社会学 天才の閃きから巨大機構の統治へ：1200時間の計算、700ページの手計算検査、そして現代LLM推論が突きつける「証明責任」再編の174年史 要約（Executive Summary） 1976年7月、イリノイ大学のケネス・アペルとヴォルフガング・ハーケンは、1世紀以上にわたり数学界を悩ませてきた「四色問題」を解決したと発表しました。しかしその実態は、単一の数学者が頭の中で一望できるエレガントな演繹ではなく、約1,200時間のメインフレーム計算と、1,482個もの可約配置、そして487の放電規則に基づく700ページにおよぶ手作業の泥沼パッチワークでした。本書の前半では、1852年の問題提起からケンペの美しい誤謬、ヘーシュの放電法による工学化、冷戦期メインフレーム計算資源の政治経済学、そして家族総出の不可視な照合労働に至る歴史を詳細に追跡します。これは単なる「機械の勝利」ではなく、発見、検証、理解、そして正当化の責任が複数の主体と装置へと解体・再配置された、数学認識論における決定的な転換点なのです。 要旨・本書の目的と構成 本書の目的は、四色定理の機械支援証明を「コンピュータが数学者を超えた特異点」として神話化することではありません。むしろ、数学的正当化の根拠が、単一の精神による「一覧的理解（サーベイアビリティ）」から、人間・アルゴリズム・ハードウェア・査読組織が織りなす「制度的監査可能性」へと移行した過程を明らかにすることにあります。この視座は、現代の深層学習・大規模言語モデル（LLM）と対話型定理証明系（Lean 4やCoq）がもたらす知能の変容を解読するための決定的な歴史的足場を提供します。 目次（Contents） フロントマター（前付） イントロダクション：知能の英雄から制度へ 方法論：STSと計算機科学史・認識論の複合アプローチ 登場人物紹介 時系列：1852–2026 演繹と計算の174年史 歴史的位置づけ・先行研究の整理 ...