20個のCodexアカウントを並列実行して20個のErdős問題の解決に挑む

27 Erdős 問題 0 Frontier Math 問題 0 Millennium 問題 Star Fleet は、Lean 4 を使用して世界で最も難しい未解決の数学的問題を解決する AI システムです。これは、最大 20 個のカスタムエージェント型ハーネス（「スターシップ」）を並列で制御する Mac デスクトップアプリであり、それぞれが専用の 60-vCPU サーバー上で GPT-5.6 インスタンスを実行し、個別の数学的問題に取り組んでいます。すべて TypeScript & Bun でゼロから構築されています。 各スターシップは以下にアクセスできます。 数千の独立したシングルコアジョブにシャーディングする検索プログラム用の最大 2,000 vCPU の x86-64 CPU バースト 大規模並列検索プログラム用の H100 GPU バースト 世界最大のコーパス（確認した限り）の Lean 4 の前提（定理と補題）で、gemini-embeddings-2 & chroma ベクトル DB を介してプレーンイングリッシュで検索可能 arXiv.org の研究論文と GitHub リポジトリの Firecrawl.dev インデックス Claude Fable API をプルーフベリファイアエージェント型ハーネスでラップし、提出された回答をレビュー + Fable の承認後に Colin（人間）に追加レビューを依頼するための iMessage API Ton 618、検証済みの Lean 4 前提（定理または補題）がすべて依存関係グラフに織り込まれ、証明が累積するローカル長期記憶システム SAT/SMT ソルバー（CaDiCaL, kissat, Z3）、Google の CP-SAT、コンピュータ代数システム（SageMath, PARI/GP, GAP, Macaulay2）、および完全な Rust, CUDA C++, Lean 4 ツールチェーンがプリインストールされた専用の 60-vCPU、120 GiB メモリサンドボックス すべて 650 Erdős 問題 630 Frontier Math 14 Millennium 問題 6 ソリューション提案（27） 「未解決」とされている多くの問題には、すでにオンラインで入手可能な非公式または部分的な回答があります。私たちは、そのような問題に取り組むことを極力避けました。 1) Erdős 問題 #123 Erdős 問題 www.erdosproblems.com/123 ›質問 a,b,c≥1 が互いに素な 3 つの整数であるとします。すべての大きな整数は、互いに割り合わない akblcma^kb^lc^makblcm (k,l,m≥0k,l,m≥0k,l,m≥0) の形式の異なる整数の和として表せますか？ (Erdős 問題 #123 — 賞金: $250 — 数論 — https://www.erdosproblems.com/123) ›結果 互いに素な整数のトリプル a,b,c>1 について、十分に大きな整数はすべて、互いに割り合わない a^i b^j c^k の異なる項の和として表されます。Lean では、これは定理 Erdos123.erdos_123 : Erdos123.IntendedStatement.def IntendedStatement : Prop := ∀ a b c : ℕ, 1 < a → 1 < b → 1 < c → PairwiseCoprime3 a b c → IsDComplete (Smooth3 a b c) /-- 非退化な仮説 `a,b,c>1` に対する Erdős 問題 123。 -/ theorem erdos_123 : IntendedStatement := intended_erdos_123 ›レポート Erdős 問題 123 の解決 問題と、それが通常の帰納法で解決できなかった理由 互いに素な整数 a,b,c>1 について、a^i b^j c^k (i,j,k≥0) の数を考えます。問題は、互いに割り合わないという追加の要件を満たしつつ、すべての十分に大きな整数がそのような異なる数の和として表せるかどうかを問うています。割り算の条件が真の難しさの源です。通常の完全性の議論は、異なるスケールから多くの項を使用できますが、異なるスケールからの項は割り算によって比較される傾向があります。逆に、割り算の反鎖として選択されたセットは、整数を埋めるには算術的に疎すぎる可能性があります。以前の研究では強力な削減スキームが開発されていました。1 つの基数での剰余を満たす補正を選択し、それを引き、その基数で割り、帰納します。特定のトリプルについては、これは有限のコンピュータチェックの後に成功します。一般的には、粘り強い有限シードの問題が残ります。まず、乗法的に広い区間 [N,CN] のすべての整数を表す必要があります。補正帰納法はこの区間を構築しません。それはそれを伝播させるだけです。これが、魅力的な部分的なアイデアが問題を完了できなかった理由のいくつかを説明しています。差が 1 の符号付き恒等式は 2 つの連続した和を与えますが、クラスごとの剰余代表者は少なくともモジュラスマイナス 1 の広がりを持つ必要があります。幅 1 の区間は、通常の剰余接着の下では成長しません。原始的なレベルでの完全剰余系は合同を解決しますが、それらの数値的な広がりについては何も語りません。Van der Waerden と Hales–Jewett の議論は、原始的な和の任意の長い算術的進行を生成しますが、当初は制御されていない公差で生成されます。公差を固定した後でも、進行 B0+rd は大きな正のベースライン B0 を運びます。そのような進行を複製すると、幅とベースラインが同じ速度で増加するため、帰納法に必要な乗法的に広いシードを生成する必要はありません。重要な教訓は、大きな加法的な幅だけでは不十分であるということでした。下限は定量的に制御下に置く必要があります。 均質なレベル座標系 最初の構造的単純化は、i+j+k=D の 1 つの均質な指数レベルで作業することです。1 より大きい互いに素な基数では、単項式の割り算はそれらの指数の座標ごとの比較です。したがって、同じレベルの 2 つの異なる単項式は互いに割り合うことはできません。均質なレベルのすべてのサブセットは自動的に原始的です。これにより、問題はサブセット和に関する加法的な問題に変わり、原始性は実質的に無料になります。構築のすべての部分を同じ正確な次数に配置できる限りです。エッジコード構築は、異なる剰余を持つ 1 つのレベルで cnc^ncn 個の原始的なサブセット和を提供し、持ち運びを制限します。その持ち運びによる色付けと、Mathlib の Hales–Jewett 定理から得られる有限の van der Waerden の適用により、原始的な均質なサブセット和の任意の長い正確な算術的進行が得られます。 1 つの AP を大きな格子区間に変換する 基数を 1<a<c<b の順に並べます。H=edgeDigitDepth(c), u=H+2 と選択し、次に 2bav≤cv となるような v>0 を選択します。A=a^{u+v}, B=b^u c^v と定義します。1 つの AP の数字ファミリのコピーは、重み A^{M-r}B^r で翻訳されます。u>H+1 の選択は、異なるコピーを b の指数における分離した帯に配置します。すべての項を abc で乗算すると、すべての AP 項が厳密な内部になります。すべてのコピーは、1 つの正確な指数次数に配置されます。有界均質基底補題は、係数和 ∑r=0MsrAM−rBr, 0≤sr<4AB が、幅 2ABM+1 以上の完全な区間を含むことを証明します。各係数を対応する AP 数字セットに置き換えることにより、これはステップ abc dabc、ここで d は AP の差である格子上の区間として実現されます。 顔補正で剰余を埋める 次の要素は、任意の指定されたモジュラスに対する剰余ごとに、任意の十分に高い正確な次数で原始的な補正を構築します。補正は 3 つの座標面でサポートされており、順序付けられたケースでは、合計サイズは CcorrcD で制限されます。これを abc dabc のモジュラスで、AP 基底構築と同じ正確な次数で適用します。面サポートの補正は、厳密な内部 AP 項とは分離されています。さらに、B/c^{u+v}=(b/c)^u>1 なので、指数支配は CcorrcD=o(BM) を与えます。したがって、補正の広がりは最終的に基底の幅よりも小さくなります。剰余接着は、格子区間を通常の連続区間 [LM,UM] に変換します。ここで、abc BM≤UM−LM, LM≤KBM+1 が固定定数 K に対して成り立ちます。この段階で、実際の区間がありますが、その乗法的な幅は定数によってのみ制限されます。これはまさに以前のベースラインの問題が残っていた場所です。 決定的なブレークスルー: オプションの内部シェル 決定的なアイデアは、同じ正確なホモ（モノミアル）まだ使用されていないものを利用することでした。