Univalent FoundationとUniMath

【 広がるビジョン 】

2017年に亡くなったVoevodskyは、Milner予想、Bloch-Kato予想を解くなど、代数幾何でグロタンディックが進もうとした道で、大きな業績を残した天才数学者です。

彼の最後の仕事は、数学の基礎とコンピュータという二つの世界に関係していました。

前回取り上げた数学での「間違った証明」の問題ですが、彼も、苦い経験がありました。

2000年頃、彼は1993年に自分が発表した論文の重要な補題が間違っていたことに気づきます。でも、その頃には、その論文は広く出回っていて、多くの数学者がその証明を「信じて」いました。彼が、その間違った補題なしでも、論文の結論が正しいことを証明できたのは、2006年になってからでした。

別のこともありました。1998年に共著で彼が発表した論文の証明に対して「正しくない」という批判が出されるのです。結論的には、彼は、正しかったのですが、彼が、最終的に、自分が正しいことを確信できたのは、2013年になってからでした。

Voevodskyは、考えます。「数学が、累積的（accumulative）な性格を持つのなら、もしも、そこに誤りが紛れ込むと、それも、累積する可能性がある。」と。

こうした問題に対する、Veovodskyのとった対応はラジカルで驚くべきものでした。

彼は、数学をその基礎から改めて考えなおしたのです。そして、集合論に変わる新しい数学の基礎づけ Univalent Foundationを構築します。

さらに、彼は、数学の証明に、コンピュータを使うべきだと主張した最初の数学者となりました。そして、そのためのコンピュータによる証明支援システムのライブラリーUniMthを開発しました。

彼の考えたことを、少し長くなりますが、彼のインタビュー記事から引用します。

彼は、「数学は今、危機的状況、いや、2つの危機に瀕している」といいます。

「第一は、それは、「純粋数学」と「応用数学」の分離に関連しています。

遅かれ早かれ、実用性のないことに従事している人たちに、なぜ社会がお金を払わなければならないのかという疑問が生じるのは明らかでした。

第二は、あまり明らかではありませんが、純粋数学の複雑さに関連しています。

遅かれ早かれ、論文が複雑すぎて詳細な検証ができなくなり、発見されないエラーが蓄積される過程が始まるということです。そして、数学は非常に奥の深い学問であり、ある論文の結果が、通常、何本も何本も前の論文の結果に依存するという意味で、数学にとってのこの誤りの蓄積は非常に危険です。

そしてすぐに、唯一の長期的な解決策は、私が抽象的、論理的、数学的に構築したものを、コンピューターを使って検証できるようにすることだということが明らかになりました。」

ただ、すぐにコンピュータが使えたわけではありません。当時、そうしたツールは存在しなかったし、何よりも、そうした手段を使うには、数学の基礎づけ自体が、不十分なものでした。

「既存の基礎体系には2つの大きな問題があり、それらは不十分なものでした。
第一に、既存の数学の基礎は、述語論理の言語に基づいており、このクラスの言語はあまりにも限定的でした。第二に、既存の基礎は、例えば、私の2-theoryに関する研究のような対象に関する記述を直接表現するために使用することができませんでした。」

こうして彼は、彼が発見したUnivalence Axiomを中心とするHomotopy Type Theoryを武器に、集合論・カテゴリー論論に代わるUnivalent Foundationという数学の新しい基礎付けを開始することになります。

興味深いのは、彼が、こうした理論展開を、数学論文ではなく、Coqのプログラムの形でGitHubで公開したことでした。https://github.com/vladimirias/Foundations/

今回は、触れることはできませんでしたが、Univalence Axiomについては、丸山の次の資料を参照してください。「「同じ」を考える -- 「型の理論」入門」https://www.marulabo.net/docs/type-theory/　

彼は、全ての数学の領域を、このUnivalent Foundationの上で、コンピュータで検証可能なプログラムとして記述して基礎づけようとします。この壮大なプロジェクトがUniMathです。20世紀に、ブルバキがやったことを、本ではなくコンピュータのプログラムとして展開しようとしたのです。

UniMathについて、彼は次のように述べています。

「UniMathは構成的数学のライブラリですが、アルゴリズムに関するものではありません。ユーザーは、UniMathをコンパイルされたコードの形で見ることはありません。

その価値は、さまざまなユーザー入力に対応して、さまざまなアウトプットを提供する能力にあります。

UniMathは、ソースコードの形で存在します。UniMathを「使う」ことは、既存のソースコードを拡張して新しいソースコードを書くことです。

それを行うためにには、以前に書かれたソースを読み、それをを理解しなければなりません。

人によって、UniMathを使う目的は様々でしょう。

ある人は、複雑な数学の証明を検証したいかもしれません。

ある人は、数学のある古典的領域の問題を、構成主義的数学に枝分かれさせるのに使いたいと思うかもしれません。

ある人は、学生に厳密な数学とは何かを教えるための教材として使うかもしれません。」

以前、数学的発見が、コンピュータの世界におちてくるまで、40年近い「タイムラグ」があるという話をしました。ただ、今回のVeovodskyによる数学の新しい基礎の発見には、こうした「タイムラグ」はありません。発見した数学者自身が、コンピュータのライブラリーを開発し、公開しているのですから。数学とコンピュータの距離は、大きく近づきました。

きわめて残念なことに、Veovoskyは、とつぜんなくなります。

UniMathの開発は、Veovodskyの死によっ、一旦中断するのですが、後継者たちによってその開発は継続されています。

重要なことは、彼のUniMathのビジョンは、大きく広がろうとしていることです。

coqではなくlean上で開発されているのmathlib という数学の証明支援のライブラリーがあります。彼のビジョンは、mathlibのコミュニティによっても受け継がれていると思います。

“The Lean Mathematical Library”https://arxiv.org/pdf/1910.09336.pdf 

https://github.com/leanprover-community/mathlib　

コンピュータに数学の問題を解かせようとした OpenAIのプロジェクト"Theorem Prover"の最大の「学習データ」は、実はこのmathlib のソースコードそのものでした。

ChatGPTの成功の影に隠れて、ほとんど注目されることはなかったのですが、Ilya自身の肝煎りで、こうしたプロジェクトが進行していたことに、僕は注目しています。

コンピュータと数学の距離は、かつてないほど縮まっているのです。

-------------------------------------

「 Univalent FoundationとUniMath 」を公開しました。

https://youtu.be/A0qVr-vgHe8?list=PLQIrJ0f9gMcMMwP2zBgMe3LbaDnKGG_zw

資料pdf

https://drive.google.com/file/d/15pZlzUEXjo_67z567U65X5TMhobQVPCZ/view?usp=sharing

blog：「広がるビジョン 」

https://maruyama097.blogspot.com/2023/03/univalent-foundationunimath.html

「人工知能と数学」まとめページ

https://www.marulabo.net/docs/aimath/

セミナーの申し込み
https://ai-math.peatix.com/