過去・現在・未来

【 セミナーの構成について -- Voevodskyの仕事を考える 】 これまでの第一部では、コンピュータに証明問題を解かせる試みとして、Open-AI Theorem Proverを紹介してきました。 これからの第二部では、数学者が証明問題を解くのに、コンピュータを利用し始めていることを紹介して、数学へのコンピュータ利用の背景とその意味を考えようと思います。 前者では、問題を解く主体はコンピュータですが、後者では、問題を解く主体は、人間＝数学者です。 数学の証明を記述するスタイルは、今、大きく変わろうとしています。これは、21世紀の数学を特徴づけるものになるだろうと僕は考えています。 第三部では、こうした流れを切り拓いた天才 Voevodskyの数学の基礎についてのUnivalent foundationsという考えを紹介します。 彼のプロジェクト UniMathは、コンピュータで検証可能なスタイルで数学を記述しようとする、初めての試みです。 https://github.com/UniMath/UniMath 　 Univalent foundationsの中核である Homotopy Type Theoryについては、別のシリーズを予定しています。 「カテゴリー論入門」セミナーについて https://www.marulabo.net/category-theory/ 　 今回のセミナーでは、Open-AI Theorem ProverのようないわゆるAIがコンピュータに「推論能力」を与えるのではなく、そもそもコンピュータ自身が、「推論能力」を持っているという立場で議論を進めたいと思っています。 【「セミナーの構成について -- Voevodskyの仕事を考える 」を公開しました 】 https://youtu.be/4SNHi4K-2eA?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのpdfは、こちらからアクセスできます。 https://drive.google.com/file/d/1vza1sCNErB7T1eybCEqU-AFwGBAqw_Dr/view?usp=sharing このトピックのまとめページは、こちらです。ほぼ毎日更新されると思います。 https://www.marulabo.net/d

【 丸山、証明に失敗する 】 この間紹介した「連続体仮説」にしろ「Feit-Thompson定理」にしても、その意味を説明するのは簡単ではないのですが、今回紹介する「ケプラー予想」の意味は分かりやすいものです。 それは、箱におなじ大きさのボールを詰め込もうとした時、どのようにボールを並べたら、一番たくさんボールを詰め込めるかという問題です。ケプラーは、不規則にではなく規則的にボールを並べると一番高密度にボールを詰めこめると考えました。ある意味もっともだと思います。ただ、そのことを証明できませんでした。 紹介がおくれましたが、ケプラーというのは、あの天文学者のケプラーです。彼が、ボールの箱へのパッキング問題を考え予想を立てたのは 1611年のことでした。日本なら徳川幕府ができた頃です。 ただ、それから 300年たっても問題は解けませんでした。ヒルベルトは、1900年に20世紀の数学が解くべき23の未解決問題のリストを公開するのですが、「ケプラー予想」は、その18番目にランクインしています。それでも問題は解けませんでした。 ケプラーから数えれば400年たった 2014年、ヘイルズがこの問題を解決します。 彼は、不規則なボールの配置のパターンを数え上げ（5,000パターンぐらいあるそうです）、その全てのパターン総当たりで、詰め込みの密度の最小値を線形計画法を使って計算します。線形計画法の100,000個のプログラムが必要だったようです。 もちろん、その計算にはコンピュータが使われるのですが、同時に、彼はその計算が正しいことを検証するためのプログラムを開発します。そのプロジェクトを、flyspec Project といいます。それはGitHubで公開されています。 僕は、昨日、flyspec Project をビルドしようとしました。ところがなんとプロジェクトのビルドに失敗してしまいました。僕は、ケプラー予想の証明に失敗したことになります。いつも一発でビルドが通るとは限らないので、もう少し粘ってもよかったのですが、はやばやと諦めました。 というのも、このプロジェクトのビルドに成功したとしても、そのプログラムの実行（すなわち、ケプラー予想の証明）には、5,000個のCPUを使っても、一時間かかるということが分かったからです。とても、僕のくたびれたMac一台で太刀打ちできる計算

【 数学者もブラックな冗談を言う 】 2012年、Georges Gonthierは、Coqを用いて、群論のFeit–Thompson 定理の形式的証明に成功しました。 この定理は、1962-1963年にWalter Feit と John Griggs Thompson によって証明された、群論の基本的な定理の一つです。この定理は、「奇数位数の有限単純群は可解である」ことを主張し（「奇数位数定理 = “Odd Order Theorem” とも呼ばれます ）、有限単純群の分類問題で重要な役割を果たしています。 「有限単純群の分類問題」は、Daniel Gorensteinをリーダーとする数学者の集団によって解決され、20世紀の数学の大きな成果の一つと呼ばれています。 ただ、その「証明」は、100人以上の数学者が、50年のあいだに数百の論文誌に発表した、膨大な量の「証明」の総和です。そのページ数は一万ページを超えると言われています。 証明が、あまりに膨大なので、 　「この証明を全部を読んでる数学者は、１人もいない。」 というブラック・ジョークがあるそうです。 でも、数学の証明を行うのに、過去の数学の論文を全部読む必要は、実はないのです。それについては、また別の機会に説明したいと思います。 【 「Feit–Thompson定理の形式的証明」を公開しました。 】 https://youtu.be/Uxtp0N0y3bg?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのpdfは、こちらからアクセスできます。 https://drive.google.com/file/d/1zN_-J2KbwuKs_DEeapY_0P5-rtidnH4B/view?usp=sharing このトピックのまとめページは、こちらです。ほぼ毎日更新されると思います。 https://www.marulabo.net/docs/math-proof/ セミナーへのお申し込みは、こちらからお願いします。 https://math-proof.peatix.com/

【 感慨 -- 思えば遠くに来たもんだ 】 昨日、不思議な感動的な体験をしました。 月末のセミナーに向けて、数学者が証明問題を解くのに、コンピュータを利用し始めていることを紹介しようとしているのですが、どうしても取り上げたいトピックがありました。 一年ほど前、連続体仮説の独立性をコンピュータ上で証明できたという論文が出ていました。彼らは、その証明を GitHubで公開していました。「証明」はコンピュータで実行可能な「プログラム」の形をしているのです。 昨日、それを実行してみたのです。 僕のくたびれた非力なMacは、証明の準備にとりかかりました。メッセージをみると、証明に必要な情報をたくさん集めているのがわかります。一時間ほどかかって、ようやく準備ができましたようです。「証明して」とコマンドを打ち込んだら、15分ほどで、証明が終わりました！ 不思議な気持ちになりました。 確かに、僕が命令して僕のマシンが働いたのですが、僕は「連続体仮説の独立性」を証明したのでしょうか？ 「連続体仮説」というのは、数直線上の 0と1 の間に、何個の点があるのかという問題です。カントールはこの個数についてある仮説を立てたのですが、ついには狂気にいたるまでそれを証明することができませんでした。ヒルベルトは、この問題を 20世紀の数学が解くべき問題の筆頭に掲げました。 ゲーデルは、この仮説が集合論の他の公理とは矛盾しないことを示すことができました。この問題が最終的に解いたのは、コーエンです。彼は、連続体仮説がなりたつ集合論もあれば、それが成り立たない集合論もあることを示すことに成功します。それが「連続体仮説の独立性」証明です。 arXivもGitHubもない時代でした。僕がコーヘンの論文とその準備をしたゲーデルの無矛盾性証明のレクチャーノートを手に入れるのに、田舎にいたせいもあって、3ヶ月かかりました。PCもタブレットもないので、プリンストンの真っ赤な表紙のレクチャーノートをいつも持ち歩いて、ボロボロになりました。 カントール、ヒルベルト、ゲーデル、コーエンが苦闘した問題を、こたつの上の古いMacが、一時間ちょっとで解いたのです！　かつて「連続体仮説」フェチだった僕にとっては、Open-AI の「人工知能」が、数 I レベルの「数学オリンピック」の問題のいくつかをといたことなんかより、はるかに

【 数学者、コンピュータを使い始める 】 Open-AI Theorem Prover が、どのようなデータを学習してきたかをみてきたのですが、今回紹介する mathlib-train は、特別な役割を果たしています。 量的にも、これまでみてきた訓練用データより、ひとまわり大きいのです。 　miniF2F-curriculum　 327 　synth-ineq               5,600 　mathlib-train          25,000 (25K) 質的にも、mathlib-train は一味違っています。それは、多くの数学の領域をカバーしている、Lean で書かれた数学の定理集（証明付き）です。もちろん、これを作ったのは、人間です。Lean  mathlibは、多くの数学者が参加しているオープンソースのプロジェクトです。 　"Lean mathlib" 　 https://github.com/leanprover-community/mathlib mathlib-train で訓練されたOpen-AI Theorem Proverは、見違えたように賢くなりました。イリヤたちの論文のAppendix E に、三つほどその例が出ています。 なんと、Open-AI Theorem Proverは、学習した mathlib-train とはちがった形で定理の証明を考え出したのです！　素晴らしい！ ただ、話はそれで終わらないのです。 今回のセミナーのタイトルは、「コンピュータ、数学の問題を解き始める」なのですが、それに先行したのは、Lean  mathlib のように、「数学者、コンピュータで数学の問題を解き始める」という動きでした。 一人の天才数学者が、こうした動きを決定づけました。 セミナーの後半では、こうした動きを紹介しようと思います。 【「彼は、何を学習したのか (3) mathlib-train 」を公開しました 】 https://youtu.be/NPlQ9fVc8bQ?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのpdfは、こちらからアクセスできます。 https://drive.google.com/file/d/1ux2fatO6-P3pyTp9WZ8AozwkP

【 すごい！ でも、すこし違うかも 】　 前回は、Open-AI Theorem Proverが何を学習したかということで、"miniF2F-curriculum" 、"synth-ineq"、"mathlib-train"という三つの「カリキュラム」があることを紹介しました。 今回は 、5,600の訓練用の定理からなる"synth-ineq" を、もう少し見てみようと思います。といっても、僕は、このデータを全て見た訳ではありません。イリヤ達の論文にそのデータの作り方が、Appendix  D. にサンプルが、紹介されています。 サンプルの二つ目に、次のような定理が挙げられています。 　　2a(a - 68) <= a^2 + (a - 68 )^2 (a - 68 ) の '68' という数字は、ランダムに選ばれたものです。それ自体に意味はないと思います。ただ、イリヤ達の論文で、synth-ineq の作り方を見ていると、いったん '68' が選ばれると、次のような命題も、生成されるべき定理の候補になるような気がします。 　　2a(a - 1/68) <= a^2 + (a - 1/68 )^2 　　2a(a - log 68) <= a^2 + (a - log 68 )^2          ・・・ ただ、これらは全て、次のより一般的な定理から、簡単に導かれるものです。 　　2xy <= x^2 + y^2 　（ なぜなら、(x - y)^2 >= 0 から、 x^2 - 2xy + y^2 >= 0 ですから。) この定理の学習だけでは、足りないのでしょうか？ イリヤ達が紹介しているように、不等式型の定理の生成では先行する論文があります。 "INT: AN INEQUALITY BENCHMARK FOR EVALUATING GENERALIZATION IN THEOREM PROVING" https://arxiv.org/pdf/2007.02924.pdf 　 https://github.com/albertqjiang/INT これは、なかなかすごい論文で力作です。GitHub

【 お勉強は大変だ 】 数学的証明の場合には、ゲームの場合のように、セルフ・プレイで訓練用データをいくらでも提供できるわけではないことを先に見て来ました。 それでは、Open-AI Theorem Proverには、まず最初に、どのような訓練用データが提供されたのでしょうか？ ここでは、それをみていこうと思います。もちろん、このデータを選択し提供したのは、人間です。 Open-AI Theorem Prover に与えられたのは、次の三つの訓練用データです。 　1. miniF2F-curriculum 　2. synth-ineq 　3. mathlib-train 以下、それがどんなものか概略を紹介しましょう。 1. の"miniF2F-curriculum" の主要部分は、数学オリンピックにチャレンジしようとする中高生向けに、LehoczkyとRusczykがつくった問題集 “The Art of Problem Solving” https://www.amazon.co.jp/-/en/Sandor-Lehoczky/dp/0977304566 からの抜粋です。ベンチマークの miniF2Fの試験をいい成績で通るように、人間の手で、327の問題が選ばれています。もちろん、それはLeanの言葉に変換・翻訳されています。 https://github.com/openai/miniF2F/blob/statement_curriculum_learning/lean/src/statement_curriculum_learning/aopsbooks.lean に、全体が公開されていますので、ご覧ください。 2. の"synth-ineq" は、もっと強烈です。 Leanでは「等式」の証明には、便利なtactics があります。以前のショートムービー「Open-AI Theorem Proverが行う証明」 https://youtu.be/BAvCsZFGQKQ?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg で紹介した 問題1, 問題5で利用されていた "linarith" は、そうしたtactic の一つです。 ただ、不等式の証明は、基本的には、代入・変形