テレンス・タオが AI を使って形式化した証明とは、いったい何でしょうか? PFR予想の歴史の簡単な紹介

12月5日、有名な数学者でフィールズ賞受賞者のテレンス・タオ氏は、ソーシャルネットワーク上で、多項式フライマン・ルザ予想​​（PFR）の証明を形式化したLean4プロジェクトがわずか3週間で完了し、その依存関係グラフのすべてのノードが「美しい緑色」に塗り替えられたことを発表しました。

Lean コンパイラーは、この予想が標準公理に準拠していることも報告しており、これはコンピューターと AI 支援による証明にとって大きな成功であると言えます。

しかし、多項式フライマン・ルザ予想​​とは一体何なのでしょうか?この予想の証明はなぜ数学的な問題であるだけでなく、コンピューターサイエンスにとっても重要なのでしょうか? Quantum Magazine は最近、この注目すべき数学的証明とその驚くべき形式化作業について報告し、記事の中で多項式 Freiman-Ruzsa 予想を提案し証明するプロセスを整理して普及させました。

要約すると、4 人の有名な数学者 (フィールズ賞受賞者 2 名を含む) が、「加法組合せ論の聖杯」と呼べる予想を証明しました。 1か月にわたって、テレンス・タオ氏が率いる緩やかな協力チームがコンピューター支援による証明を通じて結果を検証しました。

彼らの物語を見てみましょう。

ランダムに選択された値のセットでは、追加は野火のように、止められないほど広がる可能性があります。

このようなセットの場合、その中の 2 つの数字を追加すると新しいリストが得られ、そこに含まれる数字は元のセットよりもはるかに大きくなります。初期セットに 10 個の乱数が含まれている場合、新しいリスト (合計セットと呼ばれる) には約 50 個の要素が含まれます。 100 個のランダムな数字から始めると、合計セットにはおそらく約 5,000 個の要素が含まれます。1,000 個の数字から始めると、合計セットには 500,000 個の数字が含まれます。

しかし、初期セットに構造があれば、数字の合計ははるかに小さくなります。別の 10 個の数字のセットがあるとします。それらはすべて 2 から 20 までの偶数です。異なる数字のペアでも同じ合計になる場合があるため (たとえば、10 + 12 = 8 + 14 = 6 + 16)、合計セットには 50 個ではなく 19 個の数字のみが含まれます。この違いは、初期セットが大きくなるにつれて顕著になります。 1000 個の数字からなる構造化されたリストには、合計で 2000 個の数字しか含まれない場合があります。

1960 年代、数学者のグレゴリー・フライマンは、加法と集合構造の関係 (加法組合せ論という数学の分野を定義する重要な関係) を調査するために、より小さな集合の集合の研究を始めました。フライマンは、より小さい和を持つ集合はより大きな集合に必ず含まれ、このより大きな集合の要素は非常に規則的なパターンを持つことを証明することで、素晴らしい進歩を遂げました。しかしそれ以来、この分野は停滞している。 「フライマンの最初の証明は非常に難解で、誰もそれが正しいと確信できず、本来持つべき影響力を持たなかった」と、コレージュ・ド・フランスとケンブリッジ大学の数学者でフィールズ賞受賞者でもあるティモシー・ガワーズ氏は言う。「しかし、そこにイムレ・ルザが登場したのだ。」

ルザは1990年代に2つの論文でエレガントな新しい議論を用いてフライマンの定理を反証した。数年後、2019年に亡くなったハンガリーの著名な数学者カタリン・マートンが、「小さな合計は元の集合の構造について何を明らかにできるか」という疑問を研究しました。彼女は、集合に現れる要素の種類を数学者が探すべき構造の種類に置き換え、これにより数学者がより多くの情報を抽出できるようになると主張した。マートンの予想は証明システムや符号理論に関連しており、加法組合せ論の分野で高い地位を占めています。

カタリン・マートン

彼女の予想は「これまで理解できなかった最も基本的な事柄の一つのように思えます」とオックスフォード大学の数学者ベン・グリーン氏は言う。「それは私が関心を持っている多くの事柄にとって基本的なものです。」

グリーン氏はガワーズ氏、カリフォルニア大学サンディエゴ校のフレディ・マナーズ氏、カリフォルニア大学ロサンゼルス校のフィールズ賞受賞者テレンス・タオ氏とチームを組んだ。イスラエルの数学者でブロガーのギル・カライ氏は、これをAチーム、つまり数学者のエリートチームと呼んでいる。彼らは、11月9日に発表された論文「マートンの予想について」の中で、この予想の一種を証明した。

論文アドレス: https://arxiv.org/pdf/2311.05762.pdf

この研究には関わっていないライス大学の数学者ネッツ・カッツ氏は、この証明を「そのシンプルさが美しい」そして「まったく予想外のもの」と評した。

その後、Terence Tao 氏は Lean を通じて証明を形式化し始めました。 Lean は数学者が定理を検証するのに役立つプログラミング言語です。わずか数週間で彼は成功した。 12月5日火曜日の早朝、タオ氏はリーン氏が何の後悔もなく予想の証明を完了したと発表した。 sorry は、コンピューターが特定のステップを検証できないことを意味する、Lean の標準的なステートメントです。これは、2021年以来のこのような証明ツールにとって最も印象的な成果であり、コンピューターが理解できる方法で証明を書くことから始まり、数学者が証明を書く方法の転換点を示しています。ガワーズ氏は、これらのツールが数学者にとって使いやすくなれば、長くて面倒な査読プロセスに取って代わることができるかもしれないと述べた。

この証明の構成要素は何十年もかけて作り上げられてきました。ガワーズ氏は2000年代に最初の一歩を踏み出した。しかし、カライ氏がこの分野の「聖杯」と呼ぶものが実証されるまでには、さらに20年を要した。

グループ

マートン予想を理解するには、群の概念を理解しておくと役立ちます。簡単に言えば、グループとは集合と演算で構成される数学的なオブジェクトです。ここでは、整数の集合（無限の数の数字を含む集合）と加算の演算を想定します。 2 つの整数を加算するたびに、別の整数が得られます。加算は結合法則などの他のグループ演算にも従います。つまり、演算の順序を入れ替えることができます: 3 + (5 + 2) = (3 + 5) + 2。

グループ内では、グループのすべてのプロパティを満たす小さなセットが見つかることがあります。たとえば、任意の 2 つの偶数を加算すると、別の偶数が生成されます。偶数はそれ自体がグループであり、整数のサブグループになります。しかし、奇数は異なり、サブグループではありません。 2 つの奇数を加算すると、元のセットには含まれていない偶数が得られます。しかし、各偶数に 1 を加えるだけで、すべての奇数が得られます。このようなシフトを持つ部分群は剰余類と呼ばれます。剰余類はサブグループのすべての特性を持っているわけではありませんが、サブグループの構造の多くの側面を保持しています。たとえば、奇数は偶数と同じように均等に分配されます。

ティモシー・ガワーズ

マートンは、その和が A 自体よりあまり大きくない群要素からなる集合 A がある場合、特別な性質を持つ何らかの部分群 G が存在するだろうと推測しました。 G に対して複数のシフトを実行すると、結合すると元のセット A を含む剰余類が生成されます。さらに、彼女は、剰余類の数は和集合のサイズよりも速くは増加しないと主張し、これははるかに速い指数関数的増加ではなく、多項式関係であるはずだと考えています。

この研究の方向性は、単に好奇心を満たすためだけのもので、実用性はないと思われるかもしれません。しかし、これはサブグループの全体的な構造を理解するための簡単なテスト（集合の 2 つの要素を追加すると何が起こるか）に関連しているため、数学者やコンピューター科学者にとって非常に重要です。コンピューター科学者は、暗号化されたメッセージを一度に部分的にのみデコードできるようにしたいときに、このアイデアの一般化されたバージョンにも遭遇します。これは確率的に検証可能な証明にも現れます。これはコンピューター科学者が小さな孤立した情報を調べることで検証を実行できるという証明の形式です。

これらのいずれの場合も、構造内のいくつかの点を調べるだけで、より大きく、より高レベルの構造についての結論を導き出すことができます。たとえば、長いメッセージの一部のビットをデコードしたり、複雑な証明のごく一部を検証したりするだけで済みます。

「すべてがグループの大きなサブセットであると仮定するか、または多くの付加的な偶然の存在から必要なものすべてを導き出すことができます」と、ガワーズ氏の元学生で現在は同僚であるオックスフォード大学のトム・サンダース氏は言う。「どちらの視点も有用です。」

ルザは1999年にマートン予想を発表し、自身の貢献と功績を十分に証明しました。 「彼女はフライマンと私とは独立して、おそらく私たちより先にそれを思いついたのです」と彼は言った。「それで、彼女と話した後、私は彼女にちなんでそれに名前を付けることにしました」。とはいえ、数学者は現在これを多項式フライマン・ルザ予想​​、または PFR と呼んでいます。

ゼロとワン

多くの数学的対象と同様に、グループにもさまざまな形式があります。マートンは彼女の推測がすべてのグループに当てはまると推測した。これはまだ証明されていない。新しい論文では、これが (0, 1, 1, 1, 0) のような 2 進数のリストを要素とする特定のタイプのグループに当てはまることを証明しています。コンピューターはバイナリシステムで動作するため、このグループはコンピューターサイエンスにとって非常に重要です。しかし、加法的な組み合わせ論にも役立ちます。 「これは、いろいろなことを試して遊べるおもちゃのようなものです」とサンダース氏は言う。「ここでの代数は、整数よりもずっと簡単です。」

テレンス・タオ

これらのリストは固定長で、各ビットは 0 または 1 のいずれかです。このように 2 つのリストを追加するということは、1 + 1 = 0 という規則に従って、一方のリストの各項目をもう一方のリストの対応する項目に追加することを意味します。すると、(0, 1, 1, 1, 0) + (1, 1, 1, 1, 1) = (1, 0, 0, 0, 1) となります。 PFR は、セットがサブグループではなく、特定のグループのような機能を持っている場合に、セットがどのようになるかを調べようとします。

PFR をよりわかりやすく説明するために、バイナリ リストで構成されるセット A があると想像してください。次に、A から各要素のペアを取得し、それらを合計します。得られた合計は A の合計セットを構成し、A+A として記録されます。 A の要素がランダムに選択されると、ほとんどの合計は互いに異なります。 A に k 個の要素がある場合、和集合には k²/2 個の要素があることを意味します。 k が非常に大きい場合 (1000 など)、k²/2 は k よりもはるかに大きくなります。しかし、A が部分群である場合、A+A のすべての要素は A に含まれるため、A+A のサイズは A 自体と同じになります。

PFR で考慮されるセットはランダムではありませんが、サブグループでもありません。これらのセットでは、A+A の要素数は 10,000 または 100,000 など、やや少なくなります。 「構造の概念が単なる正確な代数構造よりもはるかに豊富な場合、これは本当に役立ちます」と、カリフォルニア大学サンディエゴ校のコンピューター科学者、シャチャー・ラヴェット氏は言う。

数学者が知る限り、この性質に従うすべての集合は「真の部分群にかなり近い」とタオ氏は言う。「他の種類の擬似群は存在しないというのは直感的に理解できる」。フライマン氏はこの命題の一種を自身のオリジナルの研究で証明した。 1999 年、ルザはフライマンの定理を整数からバイナリ リストの設定に拡張しました。彼は、A+A の要素の数が A のサイズの定数倍である場合、A は必ずサブグループに含まれることを証明しました。

しかし、ルザの定理では、部分群が非常に大きくなることが要求されます。マートンの洞察は、A が 1 つの巨大なサブグループに含まれるのではなく、元の集合 A より大きくないサブグループの多項式個の剰余類に含まれる可能性があると仮定することでした。

良いアイデアは一目でわかる

2000 年頃、ガワーズは等間隔の弦の集合に関する別の問題に取り組んでいたときに、ルザによるフライマンの定理の証明に出会った。 「それが私が必要としていたもの、つまり特定の集合に関する非常に曖昧な情報から構造化された情報を得ることでした」とガワーズ氏は語った。「ルザ氏がちょうどこの素晴らしい証明を思いついたことは、私にとって非常に幸運でした。」

フレディ・マナーズ

ガワーズはこの予想の多項式バージョンを証明しようと試みた。彼のアイデアは、比較的小さな合計を持つ集合 A から始めて、徐々に A を操作してサブグループに変えるというものでした。結果として得られたサブグループが元のセット A と類似していることを示すことができれば、その推測が正しいと簡単に結論付けることができます。ガワーズ氏は同僚らとこの考えを共有したが、誰もそれを完全な証明にすることはできなかった。 Gowers の戦略は、場合によっては成功しますが、他の場合には、A を多項式 Freiman-Ruzsa 予想の予想される結論からさらに遠ざけてしまいます。

結局、この分野ではこのアイデアは放棄されました。 2012年、サンダースはPFRをほぼ証明した。しかし、彼は多項式レベルよりもわずかに高いシフトサブグループの数を必要としました。 「彼がそうすると、それはそれほど緊急ではなくなったことを意味しますが、それでもそれは私が本当に好きな良い質問です」とガワーズ氏は語った。

しかし、ガワーズ氏のアイデアは同僚たちの記憶とハードドライブの中に生き続けている。 「あれは本当にいいアイデアだった」と、ガワーズ氏の教え子でもあったグリーン氏は言う。「いいアイデアかどうかは、見ればわかる」。この夏、グリーン氏、マナーズ氏、タオ氏はついにガワーズ氏のアイデアを地獄から解放した。

グリーン、タオ、マナーズの3人の共同作業は、ガワーズ氏の20年前のアイデアに取り組むことを決めるまでに37ページに達していた。 6月23日の論文「Sumsets and entropy revisited」では、確率論における「ランダム変数」の概念を利用して、和が小さい集合の構造を検出することに成功した。この切り替えにより、チームはコレクションをより巧妙に操作できるようになりました。 「ランダム変数を扱うのは、ある意味では集合を扱うよりもはるかに簡単です」とマナーズ氏は言う。「ランダム変数では、確率の 1 つを少し調整することができ、それによってより優れたランダム変数が得られる可能性があります。」

この確率論的な観点から出発すると、グリーン、マナーズ、タオは集合内の要素の数を扱う必要がなくなり、代わりにランダム変数に含まれる情報、つまりエントロピーと呼ばれる量を測定できるようになります。エントロピーは加法的な組み合わせ論にとって何も新しいものではありません。実際、テレンス・タオは 2000 年代後半にこの概念を普及させようとしました。しかし、誰もそれを多項式フライマン・ルザ予想​​に適用しようとはしなかった。グリーン、マナーズ、タオはそれが強力であると感じました。しかし、彼らはまだその推測を証明することができなかった。

ベン・グリーン

研究チームが新たな結果を精査するうちに、彼らはついにガワーズ氏の眠っていたアイデアを復活させることができる環境を作り出したと気づいた。要素の数ではなくセットのエントロピーを使用してセットのサイズを測定すると、技術的な詳細がはるかに扱いやすくなる可能性があります。 「ある時点で、ティムの20年前のアイデアの方が、当時私たちが試していたアイデアよりも実際にうまくいく可能性が高いことに気付きました」とタオ氏は言う。「そこで、ティムをプロジェクトに呼び戻しました。すると、すべてのピースが驚くほどうまくまとまりました。」

しかし、完全な証明ができるようになるまでには、まだ対処すべき詳細事項が数多く残っています。 「私たち4人全員が他のことで忙しかったというのは、ちょっとばかげたことでした」とマナーズ氏は言う。「この素晴らしい結果を発表して世界に伝えたいのに、実際にはまだ中間報告を書かなければならないのです。」最終的に、チームは粘り強く取り組み、11月9日に論文を発表した。彼らは、A+A が A のサイズの k 倍以下であれば、A は k¹² 以下のシフトで A 以下のサブグループによってカバーできることを示しました。この変位量は非常に大きいものとなる可能性があります。しかし、これは多項式であり、k が指数関数的である場合のように、k が増加するにつれて指数関数的に増加することはありません。

数日後、タオは証明を形式化し始めました。彼は、バージョン管理パッケージ GitHub を使用して世界中の 25 人のボランティアからの貢献を調整しながら、協力的な方法で正式化プロジェクトを実行しました。彼らはBlueprintと呼ばれるツールを使用しました。パリ・サクレー大学の数学者パトリック・マソ氏が開発したこのツールは、タオ氏が「数学的英語」と呼ぶものをコンピューターコードに翻訳する作業に使用できる。とりわけ、Blueprint では、証明に含まれるさまざまな論理ステップを説明する図を作成できます。画像内のすべての泡がタオ氏の言う「美しい緑色」に変わった時点で、チームの作業は完了した。

PFR 予想の証明の依存関係グラフ。ボックスは定義、楕円は定理と補題、背景全体が緑色で、証明が完全に形式化されていることを示しています。

論文にはごく小さなスペルミスがいくつか見つかった。タオ氏はオンラインメッセージで、「このプロジェクトの数学的に最も関連のある部分の形式化は比較的単純で簡単だったが、技術的に『明白な』ステップに最も時間がかかった」と指摘した。

マートンは、彼女の有名な予想が証明される数年前に亡くなりましたが、その証明は、エントロピーと情報理論の分野における彼女の生涯にわたる研究を際立たせるのに役立ちました。 「私がこれまで試したフレームワークよりも、このエントロピー フレームワークを研究に使うと、すべてがはるかにうまくいきます」と Gowers 氏は言います。「私にとっては、今でも魔法のようです。」