Proof by Mechanization: Cubic Diophantine Equation Satisfiability is $Σ^0_1$-Complete

この論文は、メカニズム化された証明を用いて、自然数上の単一の 3 次ディオファントス方程式の充足可能性が $\Sigma^0_1$-完全であり、したがって決定不能であることを示し、算術的証明可能性を 3 次方程式の解存在に帰着させるコンパイラと、それを固定変数を持つ単一の普遍的多項式に集約する構成を Rocq 上で検証したことを述べています。

要約

この論文は、数学とコンピュータサイエンスの非常に難しい分野（数理論理）に関するものですが、その核心は**「ある特定の種類の数式（3 次方程式）の解を見つける問題は、原理的に『不可能』である」**という驚くべき発見を、機械的に証明したという点にあります。

これを一般の方にもわかりやすく、いくつかの比喩を使って説明します。

1. 物語の舞台：「数式という巨大なパズル」

まず、**「ディオファントス方程式」**というものを想像してください。これは「整数の組み合わせを使って、ある数式を 0 にできるか？」というパズルです。

• 2 次方程式（例：$x^2 + y^2 = z^2$）： 比較的簡単で、解き方のルールが確立されています。
• 4 次方程式以上： 非常に複雑で、解があるかどうかを判定するプログラムは存在しない（＝「決定不能」）ことが昔から知られていました。

この論文の驚くべき点は、「3 次方程式」の領域です。
これまで、3 次方程式の「解の有無」を判定できるかどうかは、数学界の「聖杯」のような未解決問題でした。4 次なら無理、2 次ならできる。では、その中間の「3 次」はどうなのか？

この論文は、**「3 次方程式でも、実は『解があるかどうか』を判定する機械は作れない（決定不能である）」**と証明しました。

2. 主人公の役割：「翻訳機（コンパイラー）」

著者のミラン・ロスコさんは、ある「翻訳機」を作りました。
この翻訳機は、**「数学的な証明（『この定理は正しい』という主張）」を、「3 次方程式のパズル」**に翻訳する装置です。

• 入力： 「この数学の定理は証明できるか？」という質問。
• 翻訳プロセス： 証明のステップを一つずつチェックし、それを数式に変換します。
  • 証明の「正しさ」をチェックする単純なルールは、2 次方程式（比較的簡単）で表現できます。
  • しかし、「もし A なら B をチェックする」という**「条件分岐（もし〜なら）」**の処理を行うと、数式の複雑さが少し増え、3 次（立方）の項が生まれます。
• 出力： 1 つの巨大な「3 次方程式」。

重要なポイント：

• もし元の「数学的証明」が正しければ、この「3 次方程式」には必ず解（整数の組み合わせ）が存在します。
• もし証明が間違っていれば、解は存在しません。

つまり、「証明できるか？」という問いは、「この 3 次方程式に解があるか？」という問いと完全に同じことになったのです。

3. 決定的な矛盾：「神の機械」は存在しない

ここで、**「ゴードルの不完全性定理」**という有名なルールが登場します。
「自分自身の正しさを証明できるような、完璧な数学のシステムは存在しない」というルールです。

もし、**「3 次方程式に解があるかどうかを、一瞬で正しく判定する機械（決定機）」**が存在したとしましょう。

1. その機械を使って、翻訳機で変換された「3 次方程式」を解けば、元の「数学的証明」が正しいかどうかが一瞬でわかります。
2. つまり、その機械は「数学の真理をすべて見抜く機械」になってしまいます。
3. しかし、ゴードルの定理によると、そんな完璧な機械は存在してはいけません（存在すれば矛盾が起きる）。

結論：
「3 次方程式の解の有無を判定する機械」もまた、存在してはいけないのです。つまり、その問題は**「原理的に解けない（決定不能）」**ことが証明されました。

4. 具体的な成果：「巨大な数式」の完成

この論文は、単に「存在しない」と言うだけでなく、実際に**「9,692 個の変数を持つ、具体的な 3 次方程式」**を設計し、その係数表をコンピュータ（Rocq というツール）で厳密にチェックしました。

• 比喩： 著者は、数学の真理をすべて含み込む「万能な鍵穴」のような巨大な 3 次方程式を、実際に設計図（係数表）として作り上げました。
• この方程式に「解があるかどうか」を調べることは、結局「数学のすべての証明が正しいかどうか」を調べるのと同じ難しさを持っているため、人間もコンピュータも永遠に正解を出すことはできません。

まとめ：この論文が伝えていること

1. 3 次方程式は「境界線」だった： 2 次までは安全、4 次以上は危険、そして3 次も実は危険地帯だったことがわかりました。
2. 「証明」と「数式」は同じもの： 数学の証明の正しさをチェックする作業は、巨大なパズル（3 次方程式）を解く作業と全く同じであることが証明されました。
3. 機械化による確実性： この複雑な証明は、すべてコンピュータでチェックされ、間違いがないことが保証されています。

一言で言うと：
「数学の真理を見つけるための『3 次方程式』というパズルは、その複雑さゆえに、どんなに賢いコンピュータを作っても、その答え（解があるかどうか）を常に正しく見抜くことは永遠に不可能だ」ということを、厳密に、かつ具体的に証明した論文です。

これは、私たちが「答え」を求め続けること自体が、ある意味で「無限の迷路」に入り込むことを意味しており、数学の限界と美しさを同時に示す作品と言えます。

技術概要

Milan Rosko による論文「PROOF BY MECHANIZATION: CUBIC DIOPHANTINE EQUATION SATISFIABILITY IS Σ0 1-COMPLETE（機械化による証明：3 次ディオファントス方程式の充足可能性はΣ0 1-完全である）」の技術的概要を以下にまとめます。

1. 問題の背景と定義

この論文は、ディオファントス方程式（整数係数多項式の方程式）の充足可能性に関する古典的な問題、特に次数（degree）と変数の数の観点からの決定可能性の限界を扱っています。

• 背景: マティアセビッチ（Matiyasevich）による MRDP 定理により、ディオファントス方程式の一般の充足可能性は決定不能（Σ0 1-完全）であることが知られています。
• 既存の知見:
  • 次数 2（二次形式）: 決定可能（特定の構造を除く）。
  • 次数 4: ジョーンズ（Jones, 1980）により、58 変数の次数 4 の方程式が普遍（universal）であることが示されました。
  • 次数 3: 長年の間、次数 3 の方程式が普遍であるかどうか、あるいは単一の方程式として表現できるかが未解決でした。
• 本研究の目標: 変数の数が入力インスタンスに符号化されている場合、単一の 3 次ディオファントス方程式の充足可能性が**Σ0 1-完全（したがって決定不能）**であることを証明し、具体的な普遍的多項式を構成することです。

2. 手法とアプローチ

本研究は、形式的証明支援系 **Rocq（旧 Coq）を用いた機械化（Mechanization）**を中核としたアプローチを取っています。

2.1 算術的基盤：レジスタ算術（RA）

• 対象理論: 乗法を持たない有界算術 $I\Delta_0 + B\Sigma_1$ を制限した「レジスタ算術（Register Arithmetic, RA）」を基盤とします。言語は $\{0, S, +, =\}$ のみです。
• 乗法の表現: 乗法は原始関数ではありませんが、反復加算による $\Sigma_1$ 関係として表現可能です。これにより、RA は証明検証の基礎として機能します。
• 証明の符号化: 証明のトレース（有限列）を、**フィボナッチ基底（Zeckendorf 表現）**を用いた「キャリーレス・ペアリング（Carryless Pairing）」で符号化します。これにより、桁の繰り上がりによる複雑な相互作用を避け、次数制御を容易にしています。

2.2 コンパイラと次数制御

• 証明検証から制約系へ: 証明の検証条件（公理の一致、モーダス・ポネンス、目標式への到達）を、多項式制約系に変換する原始再帰的コンパイラを構築します。
• 次数の局所制御:
  • 構文チェックや推論検証は、原則として2 次以下の制約に翻訳されます。
  • 3 次項の発生: 3 次項は、線形な「セレクタ変数（0 または 1）」が 2 次の検証義務（例：公理マッチング）を活性化させる際（$selector \times quadratic = 0$）にのみ発生します。これにより、すべての生成された制約の次数が 3 以下に保たれます。
• 単一方程式への集約: 複数の制約を単一の方程式にまとめる際、通常は平方和（$\sum P_i^2 = 0$）を用いると次数が倍増（2 次→4 次）してしまいます。本研究では、フィボナッチ帯域を用いた混合基数（Mixed-Radix）集約法を採用し、次数を 3 のまま維持しながら単一の方程式に圧縮します。

2.3 機械化と検証

• Rocq による実装: コンパイラ、次数証明、証明検証の等価性は Rocq 内で完全に形式化され、検証されています。
• 抽出（Extraction）: 形式化されたコンパイラから OCaml 実行可能コード（cubic_checker, cubic_compiler）を抽出し、具体的な係数表を生成しています。

3. 主要な貢献と結果

3.1 単一の普遍 3 次ディオファントス方程式の構成

• 変数の数が入力に依存する単一の 3 次方程式 $P_e(\vec{x}) = 0$ が構成されました。
• この方程式の充足可能性は、RA における定理の証明可能性（$\text{Prov}_{RA}(u)$）と等価です。
• 具体的な定数表（係数テーブル）が生成され、Rocq によって次数が 3 以下であることが検証されています。
  • 変数の数: 実装例では約 9,692 変数（Definition 6.1.1）など、パラメータに応じて変化しますが、固定された有限数です。
  • 次数: 厳密に 3 以下。

3.2 Σ0 1-完全性の証明

• 定理: 単一の 3 次ディオファントス方程式の充足可能性問題は、Σ0 1-完全であり、決定不能です。
• 証明の構造:
  1. ハードネス: 任意の Σ0 1 述語（証明可能性）を、上記のコンパイラを通じて 3 次方程式の充足可能性に帰着させます。
  2. 対角線論法: もしこの充足可能性が決定可能であると仮定すると、ゲーデルの第 2 不完全性定理に矛盾する（RA が自身の整合性を証明することになる）ため、決定不能であることが導かれます。

3.3 有界普遍性と古典的普遍性

• 有界普遍性: 特定の資源制約（証明の長さや桁幅など）$k$ に対して、決定可能な「有界切片（Bounded Slice）」の方程式 $U_k$ が構成されます。
• 古典的普遍性: これらの有界切片の和集合として、完全な普遍性を再構成します。任意の RE 集合は、何らかの $k$ に対する $U_k$ の解集合として表現可能です。

4. 意義と新規性

1. 次数の閾値の解決: ジョーンズが指摘した「次数 2 は決定可能、次数 4 は普遍だが、次数 3 の状況は不明」という長年の未解決問題に対し、次数 3 が普遍であることを明確に示しました。
2. 単一方程式への圧縮: 従来の 3 次系の結果は複数の方程式の連立であったり、変数の数が非常に多かったりしましたが、本研究は**「単一の方程式」**として次数 3 の普遍性を達成しました。
3. 機械化による信頼性: 数学的な帰結だけでなく、コンパイラ、次数の保証、係数表の整合性を Rocq によって厳密に検証しています。これは「証明の証明」であり、計算論的実装と数学的証明の統合を示しています。
4. 次数制御のメカニズム: 「セレクタによる活性化」のみで 3 次項を生成し、それ以外の部分で次数を 2 以下に抑えるという精巧な設計は、ディオファントス表現の次数制御における新しい手法を示唆しています。
5. 計算論的洞察: 決定不能性の境界（次数と変数の数）が、理論内から定義できない「非予測的（impredicative）」な性質を持つことを示唆し、次数 3 が論理的資源と計算的複雑性が交差する点であることを強調しています。

結論

この論文は、ディオファントス方程式の決定可能性における「次数 3」の壁を越え、単一の 3 次方程式が計算の普遍性を担うことを、機械化された形式的証明と具体的な係数構成によって実証した画期的な成果です。これは、MRDP 定理の精密化と、計算複雑性理論と数論の交差点における重要な進展と言えます。