🔢 mathematics

Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof

本論文は、GPT-5.2 ProとAristotleシステムの組み合わせを利用し、二項係数の新たな素数ごとの解析を通じて階乗の割り切れ方における対数ギャップ現象を実証する形式的なLean証明を生成することにより、エルデシュ問題#728の初の完全自律的なAIによる解決を提示するものである。

原著者： Nat Sothanaphan

公開日 2026-01-27

📖 1 分で読めます🧠 じっくり読む

CC BY 4.0

原著者： Nat Sothanaphan

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

全体像：AI数学者チーム

伝説的な引退した天才数学者、ポール・エルデシュを想像してみてください。彼は生涯をかけて、未解決のパズルが並んだ巨大な「ToDoリスト」を残しました。そのパズルのひとつ、#728は、数十年にわたり手つかずのまま放置されていました。

最近、超知能AI（GPT-5.2 Pro）と、数学チェックに特化したロボット（アリストテレス）からなるチームが、ついにこれを解明しました。彼らは単に答えを推測したのではなく、コンピュータが100%正しいと検証できる、厳密でステップ・バイ・ステップの証明を構築したのです。この論文の著者たちは、そのコンピュータコードを、人間が読める物語へと翻訳しているのです。

パズル：階乗のバランス調整

この問題は、階乗（ $5! = 5 \times 4 \times 3 \times 2 \times 1$ のような数）に関する問いです。

$n!$ を表す巨大なブロックの山があると想像してください。あなたは、 $a!$ と $b!$ という2つの小さな塔、そして3つ目の小さな塔 $k!$ を作りたいと考えています。これら2つの小さな塔が、ブロックを余らせることなく、大きな塔の中に完璧に収まるかどうかを確認したいのです。

数学的には、これは次を意味します： $a! \times b!$ は $n! \times k!$ で割り切れるか？

パズルはこう問いかけています：「隙間（ $k$ ）」はどれほど大きくできるか？

$k$ が非常に小さい場合、ブロックを収めるのは簡単です。
$k$ が非常に大きい場合、通常は不可能です。
秘訣は、 $k$ が十分に大きく、かつブロックが収まらなくなるほど大きくはないという「ゴルディロックス・ゾーン（ちょうど良い範囲）」を見つけることです。

AIチームは、 $k$ が全体の数の**対数（ログ）**程度の大きさになるような状況が、無限に存在することを証明しました。平易な言葉で言えば：もしブロックの総数が100万個なら、隙間は約14になります。もし10億個なら、隙間は約20になります。非常にゆっくりと成長しますが、確実に成長していくのです。

戦略：「繰り上がり」ゲーム

これを解くために、数学者たちは素数（2, 3, 5, 7など）の観点から問題を見る必要がありました。彼らは、足し算における「繰り上がり」のようなルールであるクンマーの定理を用いました。

比喩：溢れ出すバケツ
特定の言語（底数 $p$ ）で数字を足していると想像してください。

2つの桁を足した結果が1つのスロットに対して大きすぎる場合、「繰り上がり」として次のスロットへ送ります。
目標： AIは、ある数（ $m$ ）を2倍にしたときに、大量の繰り上がり（バケツが繰り返し溢れ出すような状態）が発生する数を見つける必要がありました。
障害： 同時に、AIは $m$ の直後の数（ $m+1, m+2...$ など）が、「スパイク（突起）」を持たないようにしなければなりませんでした。つまり、式のバランスを崩してしまうような、ある素数による突然の巨大な割り切れやすさを避ける必要があったのです。

綱渡りを想像してみてください：

綱渡り（「繰り上がり」の条件）： 「繰り上がりに富んだ」数を選ぶ必要があります。それを2倍にしたとき、バケツが可能な限り頻繁に溢れ出すようにします。これにより、方程式が機能するための「割り切れやすさのセーフティネット」が作られます。
スパイク（「悪い」条件）： 次の数たちが、ある素数の巨大な累乗で割り切れてしまうような「スパイク」を持つ数を避けなければなりません。これらは、あなたを綱渡りから突き落とすスパイクとなります。

どのようにして解決策を見つけたのか

AIは単にランダムな数を選んだわけではありません。計数論的な議論（統計的な戦略）を用いました。

探索範囲： 彼らは膨大な数値の範囲（ $M$ から $2M$ まで）を調べました。
フィルター： この範囲内の数のうち、「悪い」数（繰り上がりが足りない、あるいはスパイクがある数）がどれくらいあるかを計算しました。
結果： 「悪い」候補の数は、その範囲内にある全候補の数よりも実際に少ないことを証明しました。
結論： 良い数よりも悪い数が少ないので、範囲内には必ず「良い」数が少なくとも1つは残っているはずです。

これは、「1,000個のビー玉が入った瓶があり、そのうち900個が赤色（悪い）であるなら、少なくとも100個は青色（良い）が残っているはずだ」と言うのと同じです。AIは、十分に大きな瓶であれば、常に「良い」ビー玉が存在することを証明しました。

なぜこれが重要なのか（論文による説明）

初のAI単独による証明： これは、AIシステムがエルデシュの有名な問題の一つを自律的に解決し、人間が検証可能な形式的な証明を作成した初めての事例です。
「対数的隙間」： 彼らは、隙間が対数的になり得ることを確認しました。論文では、数学者のテレンス・タオが示唆するように、隙間はさらに大きくなる可能性があるとも記されていますが、この証明は、確実なベースラインを確立しました。
手法： 用いられた手法（繰り上がりを数え、スパイクを避けること）は、かつてエルデシュ自身が用いた手法に似ていますが、ここではより複雑で動的な対象に適用されています。

まとめ

この論文は、AIチームがいかにして40年前の数学パズルを解いたかについての報告書です。彼らは、複雑な階乗の方程式が完璧にバランスする特定の数の集合が、常に存在することを示しました。彼らは、数字を「溢れ出すバケツ（繰り上がり）」として扱い、適切な場所で適切に溢れ出し、かつ間違った場所で溢れすぎることがないようなバケツが必ず見つかることを証明することで、この問題を解決したのです。

技術的要約：Erdős問題 #728 の解決

問題の定義
本論文は、階乗の整除性に関する制約：
$a! b! \mid n! (a + b - n)!$
の下での、ギャップ $k := a + b - n$ の最大可能サイズを調査するErdős問題 #728を扱っている。追加の制約がない場合、自明な解（例えば、 $a$ と $b$ を非常に大きく取ることで $k$ を任意に大きくできる）が存在する。この問題を非自明なものにするため、著者らは $a$ と $b$ が極端な値から離れている、具体的には $0 < \varepsilon < 1/2$ に対して $\varepsilon n \le a, b \le (1-\varepsilon)n$ であるという条件を課している。目標は、これらの制約下で $k$ が $n$ に対してどの程度大きくなり得るかを決定することである。

手法および証明戦略
証明は、階乗の整除条件を二項係数と $p$ 進付値に関する問題へと変換することで進められる。

二項係数の整除への帰着:
$n = 2m$ 、 $b = m$ 、 $a = m + k$ と設定することで、元の条件は以下の二項係数の整除条件と同等になる：
$\binom{m+k}{k} \mid \binom{2m}{m}$
これには、すべての素数 $p$ について、 $p$ 進付値が左辺の右辺以下であることを示す必要がある：
$\nu_p\left(\binom{m+k}{k}\right) \le \nu_p\left(\binom{2m}{m}\right)$
Kummerの定理による付値解析:
Kummerの定理を用い、 $\nu_p\left(\binom{2m}{m}\right)$ は、底 $p$ における $m + m$ の加算時に発生するキャリー（繰り上がり）の数として特定される。項 $\nu_p\left(\binom{m+k}{k}\right)$ は、連続するブロック $m+1, \dots, m+k$ 内の任意の項の最大付値 $V_p(m, k)$ によって抑えられる。
満たすべき核心的な不等式は以下の通りである：
$V_p(m, k) \le \kappa_p(m)$
ここで $\kappa_p(m)$ は、底 $p$ における $m+m$ のキャリー数である。
素数ごとの解析:
著者らは、 $p$ のサイズと $k$ の関係に基づき、解析を2つの領域に分割している：
- 大きな素数 ( $p > 2k$ ): この範囲では、不等式は自動的に成立する。区間の長さ $k$ が $p/2$ より小さいため、ブロック $m+1, \dots, m+k$ 内で $p$ で割り切れる数は高々1つである。もしある項が $p^J$ で割り切れる場合、底 $p$ の展開における $m$ の桁が、 $m$ を2倍にした際に少なくとも $J$ 回のキャリーを生じさせることを強制するため、条件を満たす。
- 小さな素数 ( $p \le 2k$ ): これが主要な困難である。著者らは、大きな区間 $[M, 2M]$ $[M, 2 M]$ 内の整数 $m$ $m$ を用いて、すべての $p \le 2k$ $p \leq 2 k$ に対して以下の2つの条件を同時に満たす確率論的な計数議論を用いている：
  - キャリー豊富 (Carry-Rich): $m$ の底 $p$ 展開において、最初の $L_p$ 個の位に $\lceil p/2 \rceil$ 以上の桁が多く存在する。これにより、 $m$ を2倍にした際に多くのキャリー（ $\kappa_p(m)$ ）が強制される。
  - スパイクなし (Spike-Free): ブロック $m+1, \dots, m+k$ 内のいかなる整数も、異常に高い $p$ の累乗で割り切れない（具体的には、 $V_p(m, k)$ が閾値 $J_p + t(M)$ 未満に抑えられる）。
Union Boundによる存在証明:
著者らは、キャリー条件またはスパイク条件のいずれかに失敗する整数の「悪い」集合を定義している。大きな桁の分布に関するChernoff boundと、スパイク条件に関する単純な計数を用いることで、これらの「悪い」集合の総測度が区間 $[M, 2M]$ のサイズよりも厳密に小さいことを示している。その結果、関連するすべての素数に対して同時に整除条件を満たす「良い」 $m$ が存在することが示される。

主要な結果
本論文は 定理1 (対数的ギャップ窓) を確立している：
任意の定数 $0 < C_1 < C_2$ および $0 < \varepsilon < 1/2$ に対して、以下の条件を満たす $(a, b, n) \in \mathbb{N}^3$ の組が無限に存在する：

$\varepsilon n \le a, b \le (1-\varepsilon)n$
$a! b! \mid n! (a + b - n)!$
$C_1 \log n < a + b - n < C_2 \log n$

この構成により、ギャップ $k$ は $n$ に対して対数的に成長する。著者らは、現在の証明は $k \asymp \log n$ を与えるものであるが、さらなる洗練により $k = \exp(c\sqrt{\log n})$ まで拡張できる可能性があると言及しているが、現在の記述は対数領域に焦点を当てている。

意義および主張

初のAI解決されたErdős問題: 著者らは、これが「AIシステムによって完全に自律的に解決された最初のErdős問題である」と主張している。使用されたシステムは、GPT-5.2 ProとHarmonic社の定理証明器「Aristotle」の組み合わせである。
形式検証: 証明はLean定理証明器における形式的な証明として生成され、その後、本稿に提示されている非形式的な数学へと翻訳された。
方法論的貢献: 本研究は、中心二項係数の約数に関するErdősおよびPomeranceの先行技術を拡張するものである。固定されたギャップサイズや「キャリー不足」の整数（キャリーが少ない整数）に焦点を当てた従来の研究とは異なり、本証明は、サイズ $k \asymp \log n$ の増大する窓を扱うために「キャリー豊富」な整数を構築している。
独立性: 著者らは、彼らの初期の研究の後、Carl Pomeranceが独立して同様の結果を導き出したこと、およびErdős問題 #729 および #401を解決するためにこの議論の修正版が使用されたことを述べている。

本論文は、問題を絶対的に最も強い形（より大きなギャップの可能性を示唆している）で解決したと主張しているのではなく、Erdősが提起した特定の対数的なギャップの問題の解決に成功したことを主張している。