数学のスタイルが変わる

【 数学のスタイルが変わる? 】

Voevodskyが危惧したことは、数学は、累積的（accumulative）な性格を持つので、そこに誤りが紛れ込むと、誤りも累積する危険があるということでした。彼は、それを数学の危機だと考えます。

彼は、数学への誤りの混入を避ける唯一の道は、数学の証明を、コンピュータで検証できるプログラムの形にすることであると考えるに至りました。ただ、その当時（もう21世紀に入っていたのですが）、そうした彼の考えを支持する数学者は、ほとんどいなかったと言います。

2010年頃から状況は変わり始めます。Voevodskyが提唱するHomotopy Type Theory に基づく数学の新しい基礎づけ Univalent Foundationが数学者の注目を集め始めます。2012年から2013年にかけて、プリンストン高等研究所は、"Special Year"を設定し、Univalent Foundationについての大規模な連続セミナーを開催し大きな成功をおさめます。数学者の関心は大きく広がりました。

Univalent Foundationは、数学理論として新しい内容を持つのですが、それらの理論の形式化をコンピュータ上の証明支援システムで行うことに適しているという特徴があります。特筆すべきは、Voevodsky は、Univalent Foundationに基づく数学の基礎づけ・再構成を、彼の主張に忠実に、GitHubで公開されたコンピュータ・プログラムの形で実行して見せたことです。こうして、それまで、数学でのコンピュータ利用に懐疑的だった多くの数学者の見方は変わり始めます。

コンピュータ上の証明システムは、個々の数学的証明の正しさの検証に使えるだけではありません。大規模な数学の形式化を整備することで、数学者のコミュニティが、形式化された定義や定理や証明を共有し、検索可能なライブラリーを構築することを可能になることを、数学者は気づき始めています。

21世紀の数学のスタイルは、今とは違ったものになっていくでしょう。

【 「Univalent Foundation」を公開しました 】

https://youtu.be/1zm8E2Y7vyY?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg

スライドのpdfは、次からアクセスできます。https://drive.google.com/file/d/11QOyxoN7Ym4JPCE9GQ90UpE_AHCMQlCX/view?usp=sharing

このトピックのまとめページは、こちらです。ほぼ毎日更新されると思います。https://www.marulabo.net/docs/math-proof/

セミナーへのお申し込みは、こちらからお願いします。
https://math-proof.peatix.com/