Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem

技術的サマリー：アリストテレス API を用いたイナゴ問題の形式化事例研究

問題定義
本論文は、第 50 回国際数学オリンピック（IMO 2009）の第 6 問として出題された「イナゴ問題」の形式化事例研究を提示する。この定理は、任意の $n$ 個の異なる正整数の集合 $\{a_1, \dots, a_n\}$ と、$n-1$ 個の正整数の集合 $M$（ただし、総和 $\sum a_i \notin M$）に対して、いかなる中間部分和 $S_k = \sum_{i=1}^k a_{\sigma(i)}$ も $M$ に属さないような、ジャンプの順列 $\sigma$ が存在することを述べる。この問題は、2009 年の IMO 全問題の中で平均点が最も低かったという歴史的な難易度で知られており、順列と禁止集合に関する非自明な組み合わせ論的推論を必要とする。

手法
本研究では、言語モデルによる探索、非形式的な補題の生成、および Lean 4 証明支援システム（Mathlib を使用）内での形式化を統合した自動定理証明システムであるアリストテレス APIを活用する。著者らは、アリストテレス API に対し、イナゴ問題の厳密かつ完全な証明を要求する特定のプロンプトを提供し、既知の定理としてこの問題を引用することを明示的に禁止し、有効な順列の構成を求めた。

その結果生じた成果物は、一般化された定理を含む Lean 4 プロジェクトである（厳密に $n-1$ ではなく $|M| < n$ を許容し、$0 \in M$ も許容する）。著者らは、完全に機械検証された宣言と、未解決の証明プレースホルダー（sorry）を含む宣言を区別するため、生成されたコードを詳細に検査した。

主要な結果と検証された構成要素
生成された Lean 開発は、主要定理の完全な証明を生み出さなかった。代わりに、4 つの完全に検証された補助補題と、1 つの未解決の主要定理からなるハイブリッドな成果物となった。

1. 検証された局所構成要素:

   • PS last: 最終的な部分和がジャンプの総和に等しいことを検証した。
   • PS swap: 隣接するジャンプの入れ替えが、その位置における特定の中間部分和のみに影響し、他のすべての部分和を変化させないことを検証した。
   • PS swap eq: 入れ替え後の変更された部分和の代数形式（$S_k' = S_k - a_{\sigma(k)} + a_{\sigma(k+1)}$）を検証した。
   • maximizer swap in M: 局所的な最大化の論証を検証した。これは、ある順列が特定のスコア関数 $G(\sigma)$ を最大化し、かつ入れ替え可能な位置における部分和が $M$ に属する場合、入れ替えによって得られる値もまた $M$ に属さなければならないことを確立する。

2. 未解決のグローバル構成要素:

   • 主要定理 grasshopper は、単一の sorry によって直接閉じられている。
   • アリストテレスの出力サマリーは、欠落しているステップをグローバルな数え上げ論証として特定している。局所的な補題は特定の入れ替えが $M$ への所属を強制することを示しているが、システムはこれらの事実を調整して、それらが $|M| < n$ という仮定に矛盾する少なくとも $n$ 個の異なる禁止値を生成することを証明することに失敗した。Lean ソースコードは、主要定理を個別に符号化された数え上げ補題に還元していないため、そのギャップは未証明の義務として残っている。

貢献
本論文は、2 つの主要な貢献を行う。

1. 再現可能な成果物: アリストテレス API を用いた、困難なオリンピックの組み合わせ論問題の検査可能かつ再現可能な Lean 4 形式化の試みを提供し、完全なソースコードと実行ログを含んでいる。
2. AI の限界に関する精密な分析: AI によって生成された証明の「証拠的ステータス」の詳細な分解を提供する。本研究は、AI システムが局所的、代数的、および交換に基づく推論ステップを成功裏に検証できる一方で、主要定理を閉じるために必要なグローバルな組み合わせ論的な帳簿付けを実行できないことを実証する。

意義と主張
本論文は、「検証された宣言」と「sorry によって閉じられた宣言」の区別が、AI 支援定理証明の解釈において決定的に重要であると論じる。この事例研究の意義は、局所的な証明探索は成功し得るが、グローバルな推論は未解決のまま残ることを実証している点にある。

著者らは、sorry を含む Lean ファイルの成功したコンパイルは、証明が完了したことの十分な証拠ではないことを強調する。この成果物は警告的な事例として機能する。すなわち、AI ツールは（4 つの補助補題のような）実質的で検証された数学的展開を生成できるが、証明の中核となる論理エンジン（グローバルな矛盾）の実装を依然として行わない可能性があるということだ。本論文は、信頼性の高い AI 支援形式化には、生成されたコードの存在単なる依存に頼るのではなく、証明義務と依存関係の厳密な検査が必要であると結論付けている。