バイブコーディング試行3ーABC予想の形式化ー

Lean 4 における ABC 予想形式化の進捗報告：1 sorry + 1 axiom の frontier 2 件を持つ 2026-05-20 更新版

本稿は ABC 予想の完全証明を主張しない。目的は、Lean 4 形式化で何が機械検証済みで、どこに未解決義務が残るかを、再現可能な証跡つきで公開することである。

Abstract

本稿は、Lean 4 による ABC 予想形式化の現時点の到達点を報告する。canonical scope を research/abc/lean4 として再計測した SSOT は、theorem=471、sorry=1、axiom=1、total lines=9090、files=25 である。

同日に実行した proof_map 検証では、formal state（sorry=1, axiom=1）に対して proof_map progress=99.3%（282/284 verified）となり、監査 verdict は INVALID であった。したがって本形式化は、

1. frontier は 2 件に局所化されている
2. ただし内訳は sorry 1 件と axiom 1 件である
3. よって完成主張は不可

という状態にある。

本稿の貢献は「証明完了宣言」ではなく、未解決義務を sorry と axiom の両面で明示し、攻撃対象を 2 件に圧縮した点にある。

更新履歴（Version History）

Version	Date (UTC)	Changes
v2	2026-05-20	更新履歴セクションを統一追加。本文の数値主張・測定値は変更なし。
v1	初版公開日	初版公開。計測値と主張範囲は本文の SSOT / Integrity Statement を参照。

1. 誠実性声明（Integrity Statement）

本稿で明示的に保証すること：

1. SSOT は scan_lean_tree による直接計測値のみを採用する。
2. 数値主張は artifact と一致する値のみ記載する。
3. proof_map progress は形式証明完了率と同一視しない。
4. 無条件な ABC 完全証明は未達であることを明示する。

本稿で主張しないこと：

1. ABC 予想の無条件解決
2. sorry 残存を伴う状態での完成宣言
3. proof_map 99.3% を数学的 completion ratio とする解釈

2. 公式計測値（SSOT）

指標	値
theorem	471
sorry	1
axiom	1
total lines	9090
files scanned	25

Measured: 2026-05-19T15:28:24.804504+00:00 via scan_lean_tree(research/abc/lean4)
Artifact: reports/measurements/abc-ssot-2026-05-20.json

解釈：

1. 未解決義務は 2 件まで局所化された。
2. その内訳は AMD/DickmanBridge.lean の sorry 1 件と AMD/SmoothNumbers.lean の axiom 1 件である。
3. 形式化は「複数 frontier が散在する段階」から「混成 frontier 2 件を監査可能に管理する段階」へ移行した。

3. 問題設定と形式化方針

ABC 予想の標準的な形は、互いに素な正整数 $a,b,c$（$a+b=c$）に対し、任意の $\varepsilon>0$ で高品質 triple が有限であることを主張する。

品質は

$$
q(a,b,c)=\frac{\log c}{\log \operatorname{rad}(abc)}
$$

で定義される。ここで $\operatorname{rad}(n)$ は異なる素因子の積である。

Lean 側では、上の有限性主張を直接一撃で証明するのではなく、次の分解を採る。

1. ABCTriple と品質の基礎層
2. smoothCount と cutoff（$c \le \max C(\delta)$）層
3. Dickman 側 lower bound と Rankin 側 upper bound の橋渡し層
4. cutoff から finiteness / endpoint への昇格層

この分解により、最終障害は「cutoff を埋める 2 定理」に局所化される。

以降の節では、各分解片がどの定理面に対応し、どの未解決義務に収束するかを追跡可能に記述する。

3.1 形式化対象と非対象

本稿が形式化対象とするのは、次の 3 点である。

1. 高品質 triple の有限性へ至るための cutoff 連鎖
2. その連鎖の Lean 上での定理依存関係
3. 最終 frontier（sorry 2 件）の局所化

一方で、本稿が対象外とするのは次の 2 点である。

1. 無条件完全証明の達成宣言
2. 未解決定理を隠した progress 報告

この「対象/非対象」の明示は、完成主張の誤読を防ぐための設計である。

3.2 証明フローに対応する具体式

本稿で追跡する中心不等式は次の 3 段である。

1. 高品質条件（入力）

$$
q(a,b,c) > 1 + \delta
$$

1. cutoff 目標（中間）

$$
c \le \max C(\delta)
$$

1. 有限性結論（出力）

$$
\left|{(a,b,c)\in \mathrm{ABCTriple} : q(a,b,c)>1+\delta}\right| < \infty
$$

さらに、品質の定義から次の同値変形が得られる。

（注）この変形では対数の定義域のために $c>1$ と $\operatorname{rad}(abc)>1$ を仮定する。

$$
\frac{\log c}{\log \operatorname{rad}(abc)} > 1+\delta
\quad\Longleftrightarrow\quad
\log \operatorname{rad}(abc) < \frac{1}{1+\delta}\log c
\quad\Longleftrightarrow\quad
\operatorname{rad}(abc) < c^{1/(1+\delta)}
$$

形式化上の frontier 2 件は、この連鎖のうち「高品質条件から cutoff を導く部分」に対応する。

$$
q(a,b,c)>1+\delta
;\Longrightarrow;
c\le \max C(\delta)
$$

ここが閉じると、Main 側で固定済みの昇格補題により有限性結論へ接続される。したがって未解決は「最終結論そのもの」ではなく、「cutoff 境界を確定する評価面」である。

4. Lean アーキテクチャ（主要モジュール）

モジュール	役割
AMD/Basic.lean	ABCTriple、根基、品質、基本不等式
AMD/SmoothNumbers.lean	smoothCount、maxC(δ)、cutoff surface
AMD/DickmanBridge.lean	Dickman/Rankin 橋渡し、指数型 route
AMD/Main.lean	local cutoff から global endpoint への昇格
AMD/ABCToRiemannBridge.lean	下流公開 API surface

構造上の要点は、未解決義務を Basic/Main 側に拡散させず、SmoothNumbers と DickmanBridge の 2 点に固定していることである。

4.1 依存関係の読み方

読解のための最短経路は次の通り。

1. AMD/Basic.lean で品質関数と補題の語彙を固定
2. AMD/SmoothNumbers.lean で cutoff 目標式を構築
3. AMD/DickmanBridge.lean で lower/upper の接続条件を明示
4. AMD/Main.lean で endpoint 主張へ昇格

この順序で追うと、frontier が「どの段で詰まっているか」を数学的文脈のまま把握できる。

より具体的には、各段は次の役割分担を持つ。

段	数学的役割	主ファイル	この段で確定すること	未解決との関係
1	入力の語彙固定	AMD/Basic.lean	ABCTriple, rad, 品質 $q(a,b,c)$, 基本不等式	frontier なし
2	cutoff 面の定式化	AMD/SmoothNumbers.lean	c \le \max C(\delta) を最終中間目標として明示	abc_c_le_maxC_of_high_quality がここに残る
3	解析的評価の橋渡し	AMD/DickmanBridge.lean	Dickman 側 lower と Rankin 側 upper を同じ向きに接続	abc_c_le_maxC_of_exponential_bounds がここに残る
4	endpoint 昇格	AMD/Main.lean	cutoff から finite endpoint への昇格	frontier なし

この表の見方は単純である。段 1 と段 4 はすでに固定済みで、実際に詰まっているのは段 2 と段 3 の接続面だけである。

5. 残存 frontier（証明内容の詳解）

残存する未解決義務は 2 件であり、内訳は sorry 1 件と axiom 1 件である。

file	line	kind	declaration
AMD/DickmanBridge.lean	752	sorry	theorem abc_c_le_maxC_of_exponential_bounds ... := by sorry
AMD/SmoothNumbers.lean	1262	axiom	axiom abc_c_le_maxC_of_high_quality

5.1 abc_c_le_maxC_of_high_quality

高品質条件から cutoff を直接導く主定理面。ABC 予想の核心に近く、ここが閉じれば下流の有限性主張が一気に接続される。

5.2 abc_c_le_maxC_of_exponential_bounds

Dickman/Rankin 分解 route 上の要石。旧 crossing-family の空虚ルートを排し、明示仮定を分離した誠実な theorem surface として保持している。

5.3 2 つの frontier の役割分担

2 件は同種の未解決義務ではない。

1. abc_c_le_maxC_of_exponential_bounds は解析的評価の橋渡し欠落
2. abc_c_le_maxC_of_high_quality は高品質条件から cutoff への投影を現時点では axiom として保持している

したがって閉鎖順序は、通常「exponential_bounds を先に閉じ、その後 high_quality 側の axiom を定理へ戻す」方が依存関係上自然である。

証明フロー（Proof Flow, 高詳細版）

ABC 形式化の中核は、「高品質 triple の有限性」を直接証明するのではなく、いったん cutoff 面へ落としてから finite endpoint へ持ち上げる 2 段構造にある。読者が最初に掴むべき骨格は次の 1 本である。

この図が表しているのは、frontier 2 件が「同じ場所に並んだ 2 個の穴」ではなく、解析的評価を供給する段と、それを高品質条件へ投影する段に分かれているという事実である。

5.4 ステップ 1: 入力条件を扱いやすい不等式へ正規化する

出発点は品質条件

$$
q(a,b,c)>1+\delta
$$

である。これは定義上

$$
q(a,b,c)=\frac{\log c}{\log \operatorname{rad}(abc)}
$$

なので、対数の定義域を満たす範囲では

$$
\operatorname{rad}(abc) < c^{1/(1+\delta)}
$$

という形に読み替えられる。ここで重要なのは、まだ finite statement には一歩も進んでいないことである。やっていることは、入力条件を「評価で扱える形」に正規化しただけである。

Lean 上ではこの段は主として AMD/Basic.lean の責務であり、三つ組、根基、品質、基本変形の語彙を固定する。

5.5 ステップ 2: 直接 finite を狙わず、cutoff を中間目標に採る

本形式化の設計上の核心は、最終結論

$$
\left|{(a,b,c)\in \mathrm{ABCTriple}:q(a,b,c)>1+\delta}\right|<\infty
$$

をいったん脇に置き、先に

$$
c\le \max C(\delta)
$$

を示す方針を採る点にある。これは「証明を弱めている」のではなく、有限性を示す仕事を

1. 高品質条件からサイズ境界を導く段
2. サイズ境界から有限個性へ昇格する段

に分割しているだけである。

この分割の利点は、未解決義務を finite endpoint そのものに散らさず、cutoff を導く評価層へ集中させられることにある。

5.6 ステップ 3: 解析的入力を Dickman/Rankin の接続問題として切り出す

cutoff を導くためには、smooth number 側で現れる量に対し、下からと上からの評価を同じ方向へ束ねる必要がある。そこで AMD/DickmanBridge.lean は、Dickman 側 lower と Rankin 側 upper の橋渡し面として置かれている。

ここで残っている sorry

• abc_c_le_maxC_of_exponential_bounds

は、「解析的な指数型評価を cutoff へ届く形でまとめ切る」責務を持つ。言い換えると、この sorry は finite endpoint の証明を直接止めているのではなく、まだ cutoff を主張できるだけの解析的入力が揃っていないことを示している。

5.7 ステップ 4: 高品質条件から cutoff への最終投影を行う

もう 1 つの frontier

• abc_c_le_maxC_of_high_quality

は AMD/SmoothNumbers.lean 側にあり、高品質条件から cutoff へ落とす最後の投影面を担う。役割の違いをはっきり言うと、

1. abc_c_le_maxC_of_exponential_bounds は「解析的評価を作る」
2. abc_c_le_maxC_of_high_quality は「その評価を高品質条件へ接続する」

である。

このため 2 件は対等な並列障害ではない。依存の向きとしては、通常

$$
\text{exponential bounds の整備}
\Longrightarrow
\text{high-quality から cutoff への投影}
$$

の順で読むのが自然である。

5.8 ステップ 5: cutoff が閉じた瞬間に Main 側の finite endpoint が有効化される

本稿で強調したい点は、Main 側が「まだ大きな未解決を抱えている場所」ではないことである。Main 側の役割は、cutoff が得られた後で

$$
c\le \max C(\delta)
\Longrightarrow
\left|{(a,b,c)\in \mathrm{ABCTriple}:q(a,b,c)>1+\delta}\right|<\infty
$$

という endpoint 昇格を実行することにある。したがって frontier 2 件が閉じるときの効果は、局所補題 2 本が増えるだけではない。証明連鎖全体が

$$
q(a,b,c)>1+\delta
\Longrightarrow
c\le \max C(\delta)
\Longrightarrow
\left|{(a,b,c)\in \mathrm{ABCTriple}:q(a,b,c)>1+\delta}\right|<\infty
$$

として全域で有効化される。

5.9 このフローを読むときの実践的な見取り図

読者の関心別に、追う順序は次のように分けるとよい。

1. 数学的な流れを知りたい場合
   高品質条件 → radical inequality → cutoff → finite endpoint の順で読む。
2. Lean 実装の責務分担を知りたい場合
   AMD/Basic.lean → AMD/SmoothNumbers.lean → AMD/DickmanBridge.lean → AMD/Main.lean の順で読む。
3. frontier の閉鎖順序を知りたい場合
   まず abc_c_le_maxC_of_exponential_bounds、次に abc_c_le_maxC_of_high_quality を見る。

この読み順を固定すると、「ABC 論文のどこが定義で、どこが評価で、どこが最後の障害か」が本文だけで追跡できる。したがって本稿の proof flow は、単なる進捗説明ではなく、残存 2 義務に対する作業設計図として機能する。

6. 旧 crossing ルートの数学的問題点（空虚性の特定）

旧 route では、次の衝突が生じる。

1. 証明済み Rankin 上界: smoothCount は上から抑えられる。
2. 旧 crossing 仮定: 同一量に対して strict lower crossing を置く。

この組は同一式で矛盾し、ex falso 的にしか進まない。そこで本実装では、矛盾を隠すのではなく、指数型 bounds の theorem surface へ明示的に置換した。

この点が本稿の重要修正点である。つまり「通っているように見えるが数学的には空虚」という経路を残さず、未解決として可視化した点に数学的意味がある。

7. proof_map 監査と数値整合

proof_map validation（2026-05-15）:

指標	値
total nodes	284
verified	282
progress	99.3%
formal sorry	1
formal axiom	1
verdict	INVALID

Measured: 2026-05-19T15:29:06.290109+00:00Z via proof_map_validation(problem=abc, lean_root=research/abc/lean4)
Artifact: reports/measurements/abc-ssot-2026-05-20.json

この verdict は「進捗が高い」ことと「形式状態が未完了である」ことの同時成立を示す。

8. cutoff 連鎖の数学的位置づけ

本稿の中心は、次の含意連鎖を機械検証可能な定理面に分解して保持することにある。

$$
q(a,b,c)>1+\delta
\Longrightarrow
c\le \max C(\delta)
\Longrightarrow
\left|{(a,b,c)\in \mathrm{ABCTriple}:q(a,b,c)>1+\delta}\right|<\infty
$$

この連鎖のうち、後半（cutoff から有限性）は Main 側で固定済みであり、前半（高品質条件から cutoff）に frontier が集中している。したがって理論的には、未解決点は「有限性の定義」ではなく「cutoff を導く評価層」に限定される。

9. frontier 2 件の閉鎖条件

frontier 2 件の閉鎖は、役割分担上次の順で読むのが自然である。

1. abc_c_le_maxC_of_exponential_bounds：Dickman/Rankin 接続の評価面を閉じる。
2. abc_c_le_maxC_of_high_quality：上の評価を高品質条件へ投影する。

この順序が妥当な理由は、後者が前者の評価整備を前提にするためである。したがって作業順序を反転すると依存補題の再構築が増え、証明経路が冗長化する。

10. 限界と脅威（Limitations and Threats）

本稿の限界は次の通り。

1. sorry 2 件の未閉鎖により、無条件完了主張はできない
2. proof_map が INVALID のため、可視化進捗と形式状態に不一致が残る
3. cutoff 境界の証明技術が集中しており、単一点失敗リスクが高い

脅威評価としては、特に 2 点を重視する。

1. 進捗率（99.3%）の過読による完成誤認
2. 旧 route の再導入による空虚証明リスク

対策として、publication gate と proof_map validation を同時運用し、数値整合と論理整合を分離監査する。

11. 次の work package（実行優先度順）

1. abc_c_le_maxC_of_exponential_bounds の閉鎖
2. abc_c_le_maxC_of_high_quality の bridge 分解と閉路依存除去
3. proof_map の verified/frontier 配分を formal state（sorry=1, axiom=1）に同期
4. proof_map_validation.py を PASS へ復帰

12. 再現性・添付資料

#	file	purpose
00	articles/ABC_Attachments_2026-05-13/00_INDEX.md	添付索引
01	articles/ABC_Attachments_2026-05-13/01_SSOT_Measurement_2026-05-13.md	SSOT 実測値
02	articles/ABC_Attachments_2026-05-13/02_ProofMap_Validation_2026-05-13.md	proof_map 検証
03	articles/ABC_Attachments_2026-05-13/03_Frontier_Analysis.md	frontier 分析
04	articles/ABC_Attachments_2026-05-13/04_Reproducibility_Commands.md	再現コマンド
05	articles/ABC_Attachments_2026-05-13/05_Lean_Source_Overview.md	ソース概観

13. 結語

2026-05-20 時点の ABC 形式化は、未解決義務を sorry 1 件と axiom 1 件へ正直に局所化した段階にある。したがって、現在の正しい結論は「完成」ではなく「最終障害が監査可能な形で圧縮された高密度進捗」である。

本稿は、その局所化の内容と監査状態を、再計測可能な形で公開する報告である。