A Kernel-Checked Exclusion Certificate for Erd\H{o}s Problem 647

技術要約：Erdős問題647に対するカーネル検証済み除外証明書

問題文
ErdősとSelfridgeによって提示されたErdős問題647は、$n > 24$ である整数 $n$ において、$\max_{m<n} (m + \tau(m)) \le n + 2$ （ここで $\tau(m)$ は約数関数）を満たすものが存在するかどうかを問うものである。この条件は $n=24$ では成立し、境界 $n+2$ はタイトであるが、これ以上の解は存在しないという予想が立てられている。これまでの計算探索では、セグメント化されたエラトステネスの篩（ふるい）やモジュロ簡約を用いることで $n \approx 9.17 \times 10^{18}$ までの解が除外されてきた。しかし、これらの計算は未検証のコード、ネイティブな decide タクティクス、あるいは問題固有の公理に依存しており、形式検証システムの信頼された証明カーネルの外側に位置している。

手法および証明書設計
本論文は、Lean 4における形式的証明を提示し、$24 < n \le 10^9$ の範囲における解の不在を証明する。この証明は、すべての数の完全な因数分解を必要とせずに、Leanカーネルによって効率的にチェックできるように設計された「ウィットネス・チェーン（証拠の連鎖）」証明書フォーマットに依拠している。

1. ウィットネスの定義: ターゲットとなる $n$ に対する「キル・ウィットネス（殺害証拠）」$m$ は、$m < n$ かつ $m + \tau(m) \ge n + 3$ を満たす整数として定義される。このようなウィットネスは、区間 $[m+1, m + \tau(m) - 3]$ に含まれるすべての $n$ に対して不等式を反駁する。
2. 平滑部分の最適化: カーネルの負荷を最小限にするため、ウィットネスは完全な因数分解を保存しない。代わりに、$m$ を割り切るすべての素数 $p < 1024$ の最大べき乗を保存する。
   • カーネルは、保存されたこれらの素数のべき乗の積が $m$ を割り切ることを検証する。
   • 各保存されたべき乗が最大であること（すなわち、$p^{e+1} \nmid m$ であること）を検証する。
   • $\tau(m)$ の下限を $\prod (e_i + 1)$ として計算する。
   • 倍増ルール（The Doubling Rule）: もし $m$ の残りの余因子（$1024$未満の素数で割り切れない部分）が$1$ より大きい場合、その下限を2倍にする。これは、余因子が平滑部分と互いに素であるため、もし存在すれば少なくとも2つの約数（1とその自身）に寄与するという理由から妥当である。
   • リストされた素数（$< 1024$）の素数性は、31までの素数による試し割りによって検証されるため、外部の素数判定証明を必要としない。
3. 貪欲な連鎖（Greedy Chaining）: 証明書は、貪欲に生成されたウィットネスのシーケンスである。カバー位置24から開始し、アルゴリズムは新しいカバー位置 $m + \tau(m) - 3$ を最大化するウィットネス $m \le C$ を選択する。この6,659,222個のウィットネスからなる連鎖が、区間 $(24, 10^9]$ 全体をカバーする。
4. 形式化の構造: Leanの開発は、「健全性レイヤー（チェッカーの論理を証明するもの）」と「データレイヤー（ウィットネスのリスト）」を分離している。データはLeanソースファイル内のリテラルとしてエンコードされている。カーネルは、連鎖の連続性と境界の妥当性を検証するために、これらのリテラルを評価する。

主な貢献と検証
本論文は、5つの異なる検証レイヤーと貢献を提供している：

• 公理の閉鎖性: 最終的な定理は、公理集合が正確に $\{ \text{propext}, \text{Classical.choice}, \text{Quot.sound} \}$ である状態で証明されている。そこには sorry も native decide も、問題固有の公理も含まれていない。
• 独立したリプレイ: 生成スクリプトは明示的に「信頼できないもの」とされている。試し割りを用いた第2の独立したPython実装が、すべてのウィットネスをリプレイして、素数性、順序、および倍増ルールを検証する。第3の実装は、約数関数を独立して再計算し、解の集合がOEIS A087280と一致することを確認する。
• ソースからの再現性: 異なるx86ハードウェア上の2つの独立した検証プロセスにおいて、ソースからLeanツールチェーンをコンパイルし（gcc および clang を使用）、キャッシュなしで mathlib と開発環境を再構築し、証明書ファイルを再生成した。結果として得られた .olean ファイルは、元のARMビルドとバイト単位で同一であり、SHA-256ダイジェストも一致した。
• スタンドアロン・チェッキング: コンパイルされた開発環境は、エラボレータをバイパスしてスタンドアロンの lean4checker によって再型付けされ、コンパイルされたアーティファクトの完全性が確認された。
• 欠陥のある設計の修正: 本論文は、大きな素数（$>1024$）が約数カウントを半分に減らすことを考慮できなかったために、生成器が「ギャップ最小値」で停止した設計のイテレーションについて記録している。倍増ルールを組み込んだことで、この問題が解決され、健全性を維持したまま強化できることが実証された。

結果
主要な結果は定理 1.1 である：$24 < n \le 10^9$ である整数 $n$ は、$\max_{m<n} (m + \tau(m)) \le n + 2$ を満たさない。

• この証明は、6,685,922個のウィットネスを用いて範囲 $(24, 10^9]$ をカバーする。
• $10^9$ までの証明書は約260 MBのソースコードであり、バージョン管理されたリリースアーティファクトとして提供される。
• $10^7$ および $10^8$ の範囲は継続的インテグレーション（CI）によって強制されており、$10^9$ の範囲は clang ツールチェーンの下で一度カーネルチェックされ、独立したリプレイパイプラインによって検証された。

意義と範囲
本論文は、Erdős問題647を完全に解決したとは述べておらず、また、他の研究者（Idén, Hughes, bentrd）が到達している $10^{18}$ までの計算の最前線に達したとも主張していない。

• 信頼 vs 範囲: 貢献は、範囲ではなく信頼の基盤にある。この結果は、$(24, 10^9]$ の範囲における非存在の検証を、未検証の計算からカーネルチェックされた証明へと移行させた。
• 有限 vs 無限: 本研究は、撤回された2026年1月の主張における特定のギャップに対処している。その主張は、「支配区間（domination intervals）」を用いてすべての $n > 24$ をカバーしようとしたが、それらの区間が漸近的に重なることを証明できずに失敗した。本論文は、その議論の「有限の形態」（限定された範囲をカバーすること）が、証明カーネルによって確定できる事実であることを示している。
• 将来の限界: 著者らは、手法の限界は数学ではなく、証明書のサイズとカーネルの実行時間に依存すると指摘している。範囲を $10^{10}$ に拡張するには約2 GBのソースが必要となり、$10^{12}$ では不可能です。将来の研究には、線形なウィットネス連鎖ではなく、モジュロ簡約を証明する構造的な議論が必要となる。

要約すると、本論文は、生成器の信頼性に依存せず、Leanカーネルと標準的な公理のみに依拠した、有限かつ完全に証明された $10^9$ までの除外証明という、検証された探索の新しい基準を確立している。