データホエール

データホエールの共有

最新記事: テレンス・タオ、編集者: Synced

AIはフィールズ賞受賞者にとって最も簡単に利用できるツールとなりました。

約3週間前、テレンス・タオは共同プロジェクトを提案しました。

プロとアマチュアの数学者、自動定理証明器、AI ツール、証明支援言語 Lean を組み合わせることで、4,694 個のモノイド群 (マグマ) 方程式と定理に関連する含意グラフを記述します。

これらの定理は、最大 4 つのモノイド演算を使用して表現できます。

つまり、4694個の定理の中から、4694 * (4694 - 1) = 22028942という式が意味する関係の真偽を判断する必要がある。

アドレス: https://github.com/teorth/equ..._theories/blob/main/data/equations.txt

このプロジェクトは9月25日の発表当日に開始され、現在19日間実施されている。

たった今、テレンス・タオ氏がプロジェクトの最新の進捗状況を発表しました。

解決された当初の影響の観点から見ると、プロジェクトは現在 99.9963% 完了しています。

解決する必要がある 22,028,942 個の含意関係のうち、8,178,279 個は真であると証明され、13,854,531 個は偽であると証明され、未解決のまま残っているのは 826 個だけです。

さらに、彼はプロジェクトの進捗状況を毎日個人ログに記録しました。

テレンス・タオが「クラウドソーシング」を通じて数学の新しい分野をどのように探求しているかを見てみましょう。

方程式理論プロジェクトは99.99%完了しました。

このセットでは、249 個の含意関係が誤りであると想定され、これらはすぐに誤りであることが証明されました。

コンパイル効率上の理由から、彼らはすべての証明を Lean で記録したわけではなく、592,790 個の含意関係のより小さなセットのみを証明し、その後推移性を通じてより大きな含意関係のセットを導き出しました。

たとえば、方程式 X が方程式 Y を意味し、方程式 Y が方程式 Z を意味する場合、方程式 X は方程式 Z を意味するという事実を使用できます。

彼らはまた、含意グラフの双対性を利用して、それをさらに簡単に簡素化しました。

プロジェクト ボランティアのたゆまぬ努力のおかげで、現在では含意図のさまざまな部分を調べるために利用できる優れた視覚化ツール (まだ開発中) が数多くあると Terence Tao 氏は言います。

たとえば、次の図は方程式 1491 のすべての結果を示しています: x = (y ◇ x) ◇ (y ◇ (y ◇ x ))。

テレンス・タオはこれを「オベリクスの法則」と呼んでいます。また、この法則には、式65：x = y ◇ (x ◇ (y ◇ x )) で表されるアステリックスの法則も存在します。

以下は、彼らが学習しているすべての方程式と定理、およびそれらが暗示している/暗示されている定理の数を示した表です。

アドレス: https://teorth.github.io/equa..._theories/implications/

これらのインターフェースも、ある程度は Lean と統合されています。

例えば、クリックするとObelix法則の暗黙方程式359が表示されます。これはTerence Tao氏が課題として提示したものです。彼は、Lean法ではわずか4行で証明できると示唆しました。

過去数週間で、彼はこれらの定理の多くがすでに文献に登場していることも知りました。

したがって、これらの方程式の「ガイド」がここにまとめられています。

アドレス: https://github.com/teorth/equ..._theories/wiki/Tour-of-selected-equations

たとえば、よく知られている交換法則 (式 43) と結合法則 (式 4512) に加えて、いくつかの式 (式 14、式 29、式 381、式 3722、式 3744) がいくつかのパトナム数学コンテストに登場しています。

式168は、「中心群」として知られる興味深い構造を定義しています。特に、これはエヴァンスとクヌースによって研究され、クヌース＝ベンディックスのアルゴリズムの重要なインスピレーションの源となりました。

式 1571 は指数が 2 のアーベル群を分類します。

バーコフの完全性定理によれば、ある方程式または定理が別の方程式または定理を意味する場合、それは有限回の書き換え操作によって証明できます。

ただし、必要な書き換え回数はかなり長くなる可能性があります。

上で述べたように、1491 が 359 を意味するという証明は非常に難しく、4 回から 5 回の書き直しが必要です。

さらに、式1689が式2を示唆するという証明は非常に長い。しかしながら、Vampireのような標準的な自動定理証明ツールは、これらの示唆の大部分を証明する能力を備えている。

より微妙なのは反含意関係であり、この場合には定理 X が定理 Y を意味しないことを証明する必要があります。原則的には、X に従うが Y には従わないモノイドを示すだけで十分です。

多くの場合、この反含意関係を取得するには、2、3、または 4 つの要素を持つモノイドなど、小さく有限なモノイドを検索するだけで済みます。

しかし、それだけでは不十分です。実際、彼らは反含意関係をいくつか知っているだけであり、それは無限モノイドを構築することによってのみ証明できます。

たとえば、既知のアステリックスの法則はオベリックスの法則を意味するものではありませんが、すべての反例は無限である必要があります。

興味深いことに、既知の構築方法は、集合論における有名な強制手法といくつかの類似点を持っています。これは、（部分）モノイドに「一般的な」要素を継続的に追加して、特定の特性を持つ反例を強制する手法です。

しかし、ここでの構築は集合論における構築よりもはるかに単純であることは確かです。

彼らはまた、「線型」モノイド x ◇ y = ax + by の構築からも有益な進歩を遂げました。これらの構成は可換環と非可換環の両方に存在します。

「合流」方程式の定理に関連する自由モノイド、およびより一般的には完全に書き直されたシステムを持つ定理。

したがって、未解決の含意関係の数は着実に減少し続けています。

標準的な GitHub の慣例に従い、論文はすぐに公開されました。

かなり忙しいバックエンドのセットアップと「火消し」作業を経て、プロジェクトは現在かなりスムーズに実行されています。

プロジェクトは Lean Zulip チャネルで調整され、すべての貢献は GitHub のプル リクエスト プロセスを通じて行われ、問題ベースの GitHub プロジェクトを通じて追跡されます。

他の 2 人のメンテナー、Pietro Monticone 氏と Shreyas Srinivas 氏も貴重な監督を提供しました。

以前の PFR 形式化プロジェクトと比較して、このプロジェクトのワークフローは標準的な GitHub プラクティスに従っており、おおよそ次のようになります。

Zulip での議論中に、プロジェクトを前進させるために特定のタスクを完了する必要があることが明らかになった場合（例えば、Lean の議論スレッドで既に導出されている含意証明を形式化するなど）、"issue" が作成されます（通常は Terence Tao 自身または他のメンテナーによって作成されます）。他の貢献者は、このissue を "claim" し、独立して作業を進めることができます（メインの GitHub リポジトリのローカルコピーを使用）。

その後、「プルリクエスト」を送信して、貢献内容をメインリポジトリにマージします。このリクエストはメンテナーや他の貢献者によってレビューされ、承認された場合は関連する問題がクローズされます。

さらに広く言えば、彼らはこの設定で得られたすべてのプロセスと教訓を文書化する作業に取り組んでいます。

これは、現在初期計画段階にあり、数十人の著者が参加する可能性のあるプロジェクトに関する今後の論文の一部になります。

テレンス・タオ氏は、プロジェクトの進捗に非常に満足しており、当初の期待の多くが満たされたと述べた。

科学分野では、彼らは、与えられた方程式理論が別の方程式理論を意味しないことを証明する新しい手法と構成を発見しました。また、体系的な探索を通じて発見されたアステリックスとオベリックスのペアなど、興味深い特徴を持ついくつかの珍しい代数構造も発見しました。

参加者は、あらゆるキャリア段階の数学者やコンピューター科学者から、興味のある学生や愛好家まで、非常に多様でした。

さらに、Lean プラットフォームは、人間が生成したコンテンツと機械が生成したコンテンツの両方からの貢献を統合する際に優れたパフォーマンスを発揮します。

量の点では、機械による生成が圧倒的に最大の貢献源ですが、多くの自動生成は、特定の状況で人間が行った発見に基づいており、その後、プロジェクトのさまざまなメンバーによって一般化され、形式化されることがよくあります。

ディスカッション スレッドでは、非公式な数学的証明も数多く行われましたが、これらの証明は多くの場合、Lean ですぐに形式化され、その正確性に関する論争は解消されました。

研究者は、残りの影響に対処するために、さまざまな実証済みの手法を最も効果的に展開する方法に焦点を当てることができます。

AIは補助的に活用されています。

当初、テレンス・タオ氏は、最新の AI ツールがこのプロジェクトに大きく貢献することを期待していました。

しかし、実際には、それらは二次的または補助的な方法で使用されます。

たとえば、GitHub Copilot などのツールを使用すると、Lean 証明、LaTeX ドキュメント フレームワーク、その他のソフトウェア コードの作成を加速できます。

さらに、視覚化ツールは主に Claude などの大規模モデルを使用して開発されています。

しかし、含意関係を解決するという中核的なタスクに関しては、より「伝統的な」自動定理証明器の方がパフォーマンスが優れています。

しかし、残りの約 700 の含意関係のほとんどは、従来のツールを使用した処理には適していません。

いくつかの意味合い（特にアステリックスとオベリックスに関連する意味合い）は、何日もの間、人間の専門家を困惑させてきました。

テレンス・タオ氏は、現代の AI が、残されたより困難な含意関係を解決する上でさらに重要な役割を果たす可能性があると考えています。

参考文献:

https://terrytao.wordpress.co...

ぜひ高評価をお願いします！ *トリプルタップ↓*