Vladimir Voevodsky｜ウラジーミル・ヴォエヴォドスキー
ウラジーミル・ヴォエヴォドスキー（Vladimir Voevodsky）の業績、「代数的K-理論・モチヴィック・コホモロジー」「ホモトピー型理論（HoTT）・単価基礎（Univalent Foundations）」
ウラジーミル・ヴォエヴォドスキー
ヴォエヴォドスキーの資料は、彼が所属していたプリンストン高等研究所（IAS）の個人ページや、有志によるGitHubリポジトリに集約されています。
1. 単価基礎とホモトピー型理論 (Univalent Foundations & HoTT)
晩年の彼が心血を注いだ、数学の新しい基礎付けに関する資料です。
- The HoTT Book (Homotopy Type Theory)
- 内容: ヴォエヴォドスキーが主導したIASでの共同研究の成果。数学を「型理論」で記述
- GitHub: github.com/HoTT/book (ソースコードとPDF)
- 公式サイト: homotopytypetheory.org
- UniMath (Library of Univalent Mathematics)
- 内容: 数学の証明をコンピューター（Coq）で検証可能にするためのライブラリ。
- GitHub: github.com/UniMath/UniMath
- Foundations of Mathematics (Lecture Notes)
- 内容: 2010年以降の「数学の基礎」に関する講義スライドやノート。
- 出典: IAS Vladimir Voevodsky Archive
2. モチヴィック・コホモロジー (Motivic Cohomology)
フィールズ賞受賞
- Cycles, Transfers, and Motivic Homology Theories
- 内容: ヴォエヴォドスキー、ススリン、フリードランダーによる共著。モチヴィック理論の基礎。
- 出典: IAS Archive – Publications (Item 37等)
- Motivic Cohomology (Clay Mathematics Monographs)
- 内容: マザ、ヴォエヴォドスキー、ウェイベルによる教科書的まとめ。
- 出典: Clay Mathematics Institute (PDF)
3. 公式アーカイブ
- IAS Vladimir Voevodsky Memorial Page
- 1990年から2017年までの全論文、講演スライド、未発表ノートが時系列・分野別に整理されています。
- URL: https://www.math.ias.edu/vladimir/
- 一価性公理 (Univalence Axiom):(A ≃ B) ≃ (A = B)「型AとBが同値であることと、それらが等しいことは同値である」というHoTTの核心部分です。
- A-無限大圏 (A-infinity Category):A∞-category
- モチヴィック・コホモロジーの記法:Hn(X, Z(i))(n次のコホモロジー、i次のモチヴィック複体)
- ホモトピー群:πn(X)
- 基礎論 (HoTT): The HoTT Book – 数学の新たな公理系を提唱
- 証明ライブラリ: UniMath – コンピューター化された数学。
- コホモロジー Motivic Cohomology – 生成原理の体系化。
- 全集: IAS Archive – 彼の生涯の全スライド・論文。
基本的な論理展開
伝統的数学は以下の２つの形式をとっている
1.公理が正しい。(true or false)
2.証明は公理と同型であるので正しい(true or false)
ゲーデルによると、公理は必ず矛盾がある（自分が正しいことを証明できない）
それであれば、公理（これは0か1かわからないが）という型に基づいた証明形式が公理と同型であることだけをコンピューターに証明させることはできるだろうか？それであれば、
もし公理がまちがっていれば0=0が出せるし、公理の選択が適切であれば1=1になる
(1はfalseでも2がtrueであることだけは最低限保証できる)
これは数学の大きな一歩前進になる。
少なくとも人間が査読して、1＝１だと思い込んでいたのにゲーデルがいうように歴史の後半で1≠1になってしまうのを防ぎたい。さらに1と思い込んでいたものも0であれば、ダブルの間違いを犯してしまう。一方、1=1または0=0であることを確実に証明することができれば、始まりが公理であるか、公理でないかは問題になるが、証明形式の型だけはあっていたと保証することができる。
「真理」を問わずに「生存」で選別する
残すもの、残さないもの、どちらにも関わらず、とにかく無限連鎖するシステムを構築してしまえば、公理性にかけるものは自然と摩擦で継続できなくなり、摩擦係数、損失関数が低い公理性根拠だけが生き残ることになるだろうという点で、加速装置を作ったようなものである。
ゲーデルの定理によって「外側から正しいと証明すること」が封じられた以上、数学が取れる唯一の道は、「内側からの矛盾による自壊」をフィルタリングの基準にすることでした。
- ヴォエヴォドスキーの加速装置: 「これが真理か？」と悩む時間を、「これを型として記述できるか？」という計算の時間に置き換えました。
- 記述できないもの（0=0を強行しようとして1≠1が露呈するもの）は、計算のエネルギーを失って止まる。
- 記述できるものだけが、その一貫性（公理性）を根拠に、次の連鎖へと加速していく。
さらにこの証明形式だけは保証できる世界を展開すれば、もし0=0を証明しているとしたらトポロジーの問題でどこかで摩擦係数が大きくなりすぎて止まるだろうし、1=1を証明しているとしたらそれは進むので自動的に残るだろう。これをvoevodskyはinduction pathと呼んだ。
Voevodskyのような一流の数学者でさえ、何年も間違いに気づかないことを自分で証明してしまった（内部から系が崩壊した）。どんなに客観性をきしたとしても人間に真に客観的な形式証明をすることは不可能である。人間はトポロジーランドスケープの停止を宣言することができない。「何が数学として生き残るか」を決定する権限は、すでに人間から「型チェックのアルゴリズム」へと移譲されている。
人間: 「なぜこれが成立するのか分からないが、型は通っているらしい」
システム: 「摩擦係数ゼロ。次のパスへ加速します」
かつては「人間が理解すること」が数学の存在意義でしたが、ヴォエヴォドスキー以降、数学は「人間が理解できるかどうかに関わらず、型として存続し続ける自律的なシステム」へと変質したということである。人間ができるのは、その加速装置が描き出す美しい（≒理解不能な）景色を、後から追いかけて解釈し、体系化するだけである。
1. 誤りの箇所：カプランスキー予想と直交群
間違いが見つかったのは、彼がススリン（Andrei Suslin）と共同で行っていた仕事の中でした。
- 対象: 複体（Complexes）の構成におけるテクニカルな補題。
- 内容: 1991年頃に執筆された、直交群のコホモロジーに関する論文において、あるステップの証明が不完全であり、結果として導き出された結論が厳密には証明できていないことが判明しました。
- 発覚の経緯: 彼は1999年に、自身の古い計算を再確認していた際、論理の飛躍があることに気づきました。驚くべきことに、その論文はすでに数年間、世界中のトップクラスの数学者たちによって読まれ、引用されていたにもかかわらず、誰もそのミスを指摘していませんでした。
2. 数学界の「沈黙」への恐怖
彼が最も衝撃を受けたのは、単に「自分が間違えたこと」ではなく、「世界最高の知性たちが数年間、その間違いをスルーしてしまったこと」でした。
- 信頼の崩壊: 数学が高度に抽象化・複雑化しすぎたため、査読者ですら「ヴォエヴォドスキーが言うなら正しいだろう」という権威への盲信に頼らざるを得なくなっていました。
- 直観の罠: 彼は、「直観的には正しいように見えるが、形式的には間違っている」という事態が、個人の能力を超えた「システム全体の欠陥」であると確信しました。
彼は後にこう回想しています。 「自分の仕事が正しいと確信できる人間が、世界に自分以外誰もいない（あるいは自分ですら怪しい）という状況で、どうやって数学を続けていけばいいのか？」
3. 解決策としての「単価基礎（Univalent Foundations）」
この絶望から、彼は「人間に依存しない数学」の構築へと舵を切ります。
彼は、「論文（テキスト）」を書いて人間に読ませるのではなく、「コード」を書いてコンピュータにチェックさせることだけが、数学の信頼性を取り戻す唯一の道だと考えました。
- Coqへの没頭: 2000年代半ばから、彼は研究時間のほとんどを、対話型証明アシスタント「Coq」を使って自分の過去の業績を再構築することに費やしました。
- HoTTの誕生: その過程で、コンピュータが理解しやすい「型理論」と、自身の専門である「ホモトピー論」が深く結びついていることを発見し、それがホモトピー型理論（HoTT）へと結実しました。
https://www.youtube.com/results?search_query=Vladimir+Voevodsky