ペータ・ショルツェ博士が証明に対して実に真摯なことは、前に紹介した“証明支援系が一流数学へと飛躍する”を読んだ人なら良く分かっただろうと思います。ブルバキの言葉を引用するまでも無く、古代Greeceの昔から数学とは即ち証明なんです。自らの証明に何らかの違和感を持つ場合は勿論のこと、他者から証明に疑念を持たれること自体が数学論文としては失格なんです。証明をないがしろにすることは数学をないがしろにすることと同義です。証明が自明であるという陳述だらけの論文をどこかで見たことがありますが、数学への冒涜以外の何ものでもありません。そういうものを好きな人は哲学又は宗教学をやればいいのではないでしょうか。
“証明支援系が一流数学へと飛躍する”はどちらかと言えば、ショルツェ博士に焦点を当てた記事でした。もう少し他の関係者にも触れた記事としてNature誌に掲載されたMathematicians welcome computer-assisted proof in ‘grand unification’ theoryがあります。私はこちらの方がいわゆる群像劇という意味合いで面白かったように思います。その記事の私訳を以下に載せておきます。
数学者達は‘大統一’理論におけるコンピュータ支援の証明を歓迎する
証明支援プロゥグラァムは抽象的な概念を処理して、数学でのソフッウェアのより大きな役割を明らかにしている。
2021年06月18日 Davide Castelvecchi
ペータ・ショルツェは現代数学の大部分を再構築したいと思い、その基礎から始めている。彼の探究の心臓部に対する証明が正しいことを思わぬ情報源から受けている。すなわち、コンピュータである。
殆どの数学者達は彼等の専門職の創造面にいつでもすぐにコンピュータが取って代わるだろうことに懐疑的であるけれども、何人かの数学者達は彼等の研究において科学技術が益々重要な役割を持つことを認めている。そして、この特別な偉業が証明支援系を認めることへの転換点となるだろう。
数論学者ショルツェは独逸のボン大学(そこに彼は本拠を置いている)での一連の講義において大掛かりな計画(コゥペンヘィゲン大学のDustin Clausenとの共同研究)を述べた。その二人の研究者達はそれをcondensed mathematics[訳注: 凝縮数学とでも訳せるのでしょうが、そのままにしておきます]と呼び、幾何学から数論まで広がる分野間の新しい見識と関係をもたらす見込みがあると言っている。
他の研究者達は注意を払っている。すなわち、ショルツェは数学の最も輝かしいスターの一人であり、革命的概念を導入している実績を持っている。Maryland州のBaltimoreにあるJohns Hopkins大学の数学者Emily Riehlは、ショルツェとClausenの展望が現実になれば、50年の間に大学院生達に数学が教えられているやり方が今日と非常に異なるだろうと言う。“将来、彼のアィディヤに影響を受けるだろうと私が思う数多くの数学分野がある”と彼女は言う。
現在まで、その展望の大部分が非常に込み入った技巧的証明に頼っているので、ショルツェとClausenでさえ正しいのか確信を持てなかった。しかし、今月の始めにショルツェは証明の心臓部を検証するための計画が特別なコンピュータソフッウェアを使って成功したと発表した。
コンピュータ支援
数学者達は長らく数値計算または複雑な式を操作するためにコンピュータを使用して来ている。いくつかの場合において、膨大な繰返し作業をコンピュータにさせることで主要な結果を証明したことがある。その最も有名なものは、地図において隣り合う国を同色で塗らない色塗りはたった四色で出来るという1970年代の証明だ。
だが、証明支援系として知られるシステムはもっと深刻である。使用者は数学概念(オブジェクッと呼ばれ、コンピュータが既に知っている、より簡単なオブジェクッに基づいている)を教えるためシステムの中に命題を入力する。命題も既知のオブジェクッとして参照され、証明支援系は現行の知識に基づいて事実が‘明らか’に真か否かを回答する。その回答が明らかでないなら、使用者はもっと詳細を入力しなければならない。このように証明支援系は議論の論理を厳密な方法で使用者が設計することを強要し、人間である数学者達が意識的か無意識的かを問わず飛ばしていた簡単な段階を埋めている。
一度研究者達が数学概念の集まりを証明支援系の中に翻訳するという骨の折れる作業をすれば、他の研究者達によって組立てられて、高度な数学オブジェクッを定義するように使用され得るコンピュータ符号のライブラリをプロゥグラァムが生成する。このようにして、人が検証するためには時間がかかり困難な、そして多分実際には不可能な場合でさえ、証明支援系は数学証明の検証を助けることが出来る。
証明支援系には長らくファンがいたが、最先端の分野において主要な役割をしたのは、これが最初であるとImperial College Londonの数学者Kevin Buzzardは言う。彼はショルツェとClausenの結果を検証する共同研究の一人だった。“残る問題はこうだった。すなわち、複雑な数学を処理出来るのか? 私達は出来ることを示した”とBuzzardは言う。
そして、それは誰もが想像したよりもずっと早く起きた。ショルツェは2020年12月に証明支援系の専門家達に対する呼びかけを陳列し、それは独逸のFreiburg大学の数学者Johan Commelinが指揮するヴォランティヤ集団により取り上げられた。06月05日(6ヶ月足らず後である)に実験の主要部分が成功したことをショルツェはBuzzardのblogに投稿した。“非常に理にかなった期間内で、難しい独創的研究を形式的に検証出来る水準に今や双方向式の証明支援系がいることを私は途方もないことだと思う”とショルツェは書いた。
ショルツェとClausenによれば、condensed mathematicsの決定的な部分は現代数学の基礎の一つである位相を再定義することにある。数学者達が研究する多くのオブジェクッが位相(つまり、どのオブジェクッの部分が同時に近いのかそうでないのかを決定する構造の典型である)を持つ。位相は図形のアィディヤを与えるが、お馴染みの学校水準の幾何のそれらよりもずっと柔軟性を持つ。すなわち、オブジェクッを引き裂かない任意の変換が許容される。例えば、任意の三角形が他の任意の三角形と位相同型(または、円とさえも位相同型)であるが、直線とは位相同型ではない。
位相は幾何学のみならず函数解析(函数の研究)においても決定的な部分を担う。函数は典型的に無限次元空間に‘住む’(波動函数のように。波動函数は量子力学にとって基本である)。また𝑝-進数と呼ばれる数体系にとっても位相は重要であり、異様な‘フラァクトゥ’位相を持つ。
大統一
2018年頃、ショルツェとClausenは位相概念に対する伝統的なアプロゥチは、幾何学、函数解析、𝑝-進数の3つの数学的世界の間に不調和を引き起こし、代わりの基礎がそれらの隔たりを埋められることを理解した。それらの分野の各々において、たとえそれらが全く異なる概念を扱っていても、多くの結果が他分野において類似物を持つらしい。しかし、一旦位相を‘正しい’方法で定義すると、理論間の類似が二人の研究者達が提案した‘condensed mathematics’と同じ実例として現れる。“それは三つの分野の或る種の大統一だ”とClausenは言う。
ショルツェとClausenはいくつかの深大な幾何学的事実のより簡単な‘condensed’証明を既に見つけており、以前には知られていなかった定理の証明を今は出来ると言う。彼等はまだこれらを公にはしていない。
しかしながら、一つの落とし穴があった。すなわち、幾何学がこの全体像の中に適合することを示すためには、ショルツェとClausenは、通常の実数の集合(直線の位相を持つ)に関する非常に技巧的な定理を証明しなければならなかった。“実数がこの新しいフレィムワーｸに入ることを許す基本定理のようなものだ”とClausenは説明する。
Clausenはショルツェが‘意志の力を通して’完了するまで、如何に冷酷に定理について考え、その過程で多くの独創的なアィディヤを生み出したかを思い起こす。“私が今まで目撃する最も驚異的な数学の離れ業だった”とClausenは思い出す。しかし、議論がとても複雑なので、ショルツェ彼自身が全体の企みを駄目にする微妙な隔たりがあるやも知れないことを心配した。“議論は説得力があったが、ただ余りにも斬新過ぎた”とClausenは言う。
その研究の検証の支援を求めて、ショルツェは数論学者仲間であるBuzzardに頼った。Buzzardは証明支援ソフッウェアパァキヂィLeanの専門家である。Leanは元々バｸﾞに対してコンピュータ符号を厳密に検証する目的のために、Washington州RedmondにあるMicrosoft Researchのコンピュータ科学者によって作製された。
BuzzardはImperialでの学部生用数学カリキュウラム全体をLeanの中に符号化する計画を長年走らせて来た。彼はperfectoid空間の概念を含む、もっと高度な数学をシステムに入れる経験もあった。perfectoid空間の概念は2018年のFields賞をショルツェにもたらすことに役立った。
Commelinは、彼も数論学者であるが、ショルツェとClausenの証明を検証するために先導した。Commelinとショルツェは彼等のLean計画を前衛的ロｸ集団Liquid Tension Experiment(両方の数学者達がファンである)に敬意を表してLiquid Tensor Experimentと呼ぶことに決めた。
続いて熱気のあるオンライン共同作業が続いた。Leanの経験を持つ12人かそこらの数学者達が加わり、研究者達はその期間にコンピュータ科学者達からの助けを得た。06月始めまでに、ティームはショルツェの証明の心臓部(彼が最も心配した部分)をLeanの中へ翻訳を終えた。そして、その証明は合っていた。つまり、ソフッウェアがその証明のこの部分を検証出来た。
より良く知る
ショルツェの証明のLean版は数万行の符号から成り、元々の版の100倍である。“Leanの符号をただ単に見れば、証明を理解することは非常に困難だろう。特に現行のやり方では”とCommelinは言う。しかし、研究者達はコンピュータで上手く行く証明を得る努力は証明をより良く理解することにも役立つと言う。
Riehlは証明支援系に経験を持つ数学者達の一人であり、証明支援系を彼女のいくつかの学部生クラーｽで教えてさえいる。彼女の研究において系統立てて証明支援系を使用しないけれども、証明支援系は数学概念を構築すること、陳述すること、それらに関する定理の証明をすることの実際だと彼女が思っているやり方を変え始めている。“以前私は、証明することと構築することは異なる2つの事柄だと思っていた。しかし今、それらは同じことだと思う”と彼女は言う。
数学者達がいつでもすぐにコンピュータに取って代わられることは多分無いだろうと多くの研究者達は言う。証明支援系は数学テクスッを読めず、人からの連続入力を必要とし、数学命題が興味深い又は深大かどうか決められない、それが正しいかどうかだけであるとBuzzardは言う。それでも、数学者達が注目し損なった一連の知られている事実をコンピュータはすぐに指摘出来るかも知れないとBuzzardは付け加えて言う。
ショルツェは証明支援系がここまで進化出来たことに驚かされたが、彼の研究において証明支援系が主要な役割を担うかどうかは分からない。“今の所、数学者としての私の創造的研究において、証明支援系が如何に役立つかあまり分からない”と彼は言う。
コメント