テレンス・タオは、インターネット上で最も強力な頭脳に報酬を提供しています! ai人間が数学の問題を覆す？ベルサイユのネット民はいなくなった
2024-09-29
한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina
【新しい知恵の紹介】最近、tao zhexuan 氏は、大多数のネチズンと数学愛好家に向けて、「人気の数学愛好家、証明アシスタント、自動アシスタント、ai が力を合わせて、数桁規模に及ぶ数学的問題を証明できるか?」という挑戦を開始しました。
テレンス・タオ氏が立ち上げた「クラウドソーシング」数学研究プロジェクトに参加してみませんか?ai支援による証明数学研究はますます実現可能になりつつある
彼らはそれぞれ、プロジェクトのさまざまな側面に精通しており、お互いの貢献を評価します。しかし、大規模な数学研究プロジェクト、特に公的寄付を伴うプロジェクトを組織したい場合は、さらに面倒になります。その理由は、全員の貢献を確認することが難しいためです。2023 年末、テレンス タオは、多項式フライマン-ルザ予想の証明を形式化した lean4 プロジェクトが 3 週間後に成功したと発表しました (写真は最新の状況を示しています)数学的引数の一部に 1 つの間違いがあると、プロジェクト全体が失敗する可能性があることに注意してください。さらに、典型的な数学プロジェクトの複雑さを考えると、学部で数学教育を受けた一般の人々に有意義な貢献を期待するのは非現実的です。このことから、数学研究プロジェクトに ai ツールを組み込むことも非常に困難であることがわかります。ai は合理的に見えても実際には意味をなさない議論を生成する可能性があるため、ai が生成した部分をプロジェクトに追加する前に追加の検証が必要です。幸いなことに、lean などの証明支援型言語は、これらの障害を克服し、プロの数学者、一般大衆、ai ツールの間のコラボレーションを可能にする潜在的な方法を提供します。このアプローチは、プロジェクトをモジュール形式で小さな部分に分割でき、プロジェクト全体を理解しなくても完了できるという前提に基づいています。現在の例には、主に既存の数学的結果を形式化するプロジェクト (最近マートンによって証明された pfr 予想の形式化など) が含まれます。これらの形式化は、主に人間の貢献者 (プロの数学者や関心のある一般の人々を含む) によるクラウドソーシングを通じて行われます。同時に、従来の自動定理証明器やより最新の ai ベースのツールなど、タスクを完了するためのより自動化されたツールを導入する新たな試みもいくつか行われています。
そして、テレンス・タオこの新しいパラダイムは、既存の数学を形式化するだけでなく、まったく新しい数学を探索するためにも使用できると考えられています。過去に、彼と彼の後継者はオンラインコラボレーション「polymath」プロジェクトを組織しましたが、これが良い例です。ただし、このプロジェクトでは証明補助言語がワークフローに組み込まれておらず、コントリビューションは人間のモデレーターによって管理および検証される必要があり、これには非常に時間がかかり、これらのプロジェクトのさらなる拡張が制限されました。現在、tao zhexuan 氏は、証明補助言語を追加することで、このボトルネックを打破できると期待しています。彼は、これらの最新のツールを使用して、一度に 1 つまたは 2 つの問題だけに焦点を当てるのではなく、あるクラスの数学的問題を同時に調査できるかどうかに特に興味を持っています。本質的に、このアプローチは反復的なタスク用のモジュール式であり、すべての貢献を厳密に調整するプラットフォームが存在する場合、クラウドソーシングと自動化ツールが特に役立ちます。この種の数学的問題は、以前の方法では拡張できませんでした。この種の問題について合理的な直観が得られるまで、何年もかけて個々の論文で一度に 1 つのデータ ポイントをゆっくりと調査しない限り。さらに、大規模な問題データ セットがあると、さまざまな自動化ツールのパフォーマンス評価を実行したり、さまざまなワークフローの効率を比較したりするのに役立ちます。今年7月、5番目のビジービーバーの数は47,176,870であることが確認された。great internet mersenne prime search (gimps) など、以前のクラウドソーシング コンピューティング プロジェクトのいくつかは、これらのプロジェクトと精神的に似ていますが、補助言語を証明するのではなく、より伝統的なプルーフ オブ ワーク メカニズムを使用しています。テレンス・タオ氏は、数学的空間を探求するクラウドソーシング・プロジェクトの既存の例が他にあるかどうか、また、得られた教訓が活用できるかどうか知りたいと述べた。この目的を達成するために、タオ自身がこのパラダイムをさらにテストするプロジェクトを提案しました。このプロジェクトは、昨年の mathoverflow の質問からインスピレーションを受けました。その後すぐに、tao zhexuan が自身の mathstodon でこの件についてさらに議論しました。この問題は普遍代数の分野に属し、元の群 (マグマ) の単純な方程式の理論の中規模の探求が含まれます。元のグループは二項演算を備えたグループですセットgです。最初は、この演算 o には追加の公理が付加されていないため、元の群自体は比較的単純な構造です。もちろん、恒等公理や結合公理などの追加の公理を追加することで、群、半群、モノイドなどのより身近な数学的対象を得ることができます。ここで、（定数なしの）等式公理に興味があります。これらの公理は、演算 o と g の 1 つ以上の未知の変数から構築された式の等価性に関係します。このような公理の 2 つのよく知られた例は、交換法則 xoy = yox と結合法則 (xoy) oz = xo (yoz) です。ここで、x、y、z は元のグループ g の未知の変数です。一方、(左) 恒等公理 eox = x は、定数 e ∈ g が含まれるため、ここでは等式公理とはみなされません。このような定数を伴う公理については、この研究では議論しません。次に、テレンス タオは、彼が始めた研究プロジェクトを説明するために、原始群に関する平等公理の 11 個の例を紹介しました。これらの等式公理は、原始的な群演算と未知の変数のみを含む方程式です。したがって、たとえば、式 7 は可換公理を表し、式 10 は結合公理を表します。定数公理式 1 は、元の群 g が最大 1 つの要素を持つように制限されているため、最も強力です。逆に、再帰公理式 11 は最も弱く、すべての元の群がこの公理を満たします。次に、これらの公理間の導出関係を調べることができます。どの公理がどの公理を導出できるでしょうか?たとえば、式 1 はこのリスト内の他のすべての公理につながり、さらに式 11 につながります。式 8 を特殊なケースとして使用して式 9 を導出し、さらに式 9 を特殊なケースとして使用して式 10 を導出できます。これらの公理間の完全な導出関係は、次のハッセ図で説明できます。この結果は、具体的には、定数公理 (式 1) と結合公理 (式 10) の間に等式公理があるかどうかという、数学 q&a web サイト mathoverflow の質問に答えます。ここでの含意関係のほとんどは証明するのが簡単であることは注目に値します。ただし、自明ではない含意関係があります。この関係は、前の質問と密接に関連する mathoverflow 投稿への回答で見つかりました。これはすべての x,y ∈ g に当てはまります。特に、y = xox の場合、(xox) o (xox) = (xox) ox となります。(1) を再度適用すると、xox は冪等であると結論付けることができます。ここで、(1) の x を xox に置き換えて (2) を使用すると、 (xox) oy = yo (xox) が得られます。さらに、(1)を2回適用すると、(xox) o (yoy) = (yoy) ox = xoyとなります。したがって、(3) は、式 7 である xoy = yox に簡略化できます。上記の議論プロセスの形式化は、lean にあります。ただし、ある等式公理のセットが別の等式公理のセットを決定するかどうかを決定するという一般的な問題は決定できないことに注意してください。したがって、ここでの状況は「忙しいビーバー」の課題に似ています。つまり、複雑さが一定の点に達すると、決定不能な問題に遭遇することになりますが、この閾値に達する前に、興味深い問題や現象を発見したいと考えています。上記のハス図は、リストされた等価公理間の含意関係を主張するだけでなく、公理間の非含意関係も主張します。たとえば、図に示すように、可換公理方程式 7 は方程式 4 (x + x) + y = y + x の公理を意味しません。これを証明するには、可換公理式 7 は満たすが、公理式 4 は満たさない原始群の例を見つけるだけです。たとえば、この場合、自然数集合 n を選択できます。その演算は xoy := x+y です。より一般的には、この図は次の非含意関係を主張しており、(すでに述べた含意関係と合わせて) これら 11 個の公理間の部分的に順序付けされた含意関係のセットを完全に記述します。ここで、tao zhexuan は、証明の一部を完成させるために反例を提案するよう読者に勧めています。見つけるのが最も難しい反例は、式 9 から式 8 を推定できないことです。さらに、tao zhexuan は、上記すべての包含関係と反包含関係のリーン証明を含む github リポジトリも提供しています。11 個の方程式のハース図を計算するだけでも、すでに少し面倒であることがわかります。terence tao によって提案されたプロジェクトは、このハス図を数桁拡張して、より広範囲の方程式セットをカバーする試みです。彼が提案した集合は ε で、和方程式の再帰性と対称性の公理がラベル付けし直されるまで、元の群演算 o を最大 4 回使用する方程式の集合です。これには上記の 11 個の方程式が含まれていますが、さらに多くのものがあります。カタロニア語の数値 c_n は、二項演算 o (n+1 個のプレースホルダー変数に適用される) を使用して式を作成する方法の数であり、m 個のプレースホルダー変数の文字列が与えられた場合、ベル数 b_m はこれらの変数の方法の数であることを思い出してください。割り当てられた名前 (再ラベル付け可能)。これにより、特定のプレースホルダーに同じ名前を割り当てることができます。したがって、対称性を無視すると、最大 4 つの演算を含む方程式の数は次のようになります。残りの 9118 個の方程式は、方程式の対称性によりペアで表示されるため、ε の合計サイズは次のようになります。
tao zhexuan 氏は、そのような id の完全なリストをまだ作成していないと述べましたが、python を使用すれば簡単に作成できるのではないかと考えています。ai ツールを使用すると、必要なコードのほとんどを生成できるはずです。彼は、ε の幾何学形状がどのようなものになるのか全く分からないと言いました。ほとんどの方程式は互いに比較できないでしょうか? 「強い」公理と「弱い」公理に分かれるのでしょうか？現在、テレンス・タオのメッセージエリアには数十のコメントが寄せられている。興味のある読者、tao zhexuan さんもあなたに招待状を差し上げています。
