Lean4: FLT n=3 証明の形式化が完了？

関連

前提仮定

ここで前提となる仮定を構築する補題群が出来ました。

仮定式

$$
\large
\forall q,\; \text{Prime } q \to q \mid (c^3-b^3) \to q \nmid (c-b) \to \neg q^2 \mid S0(c,b)
$$

hS0_not_sq

hS0_not_sq :
∀ {q : ℕ}, Nat.Prime q → q ∣ c ^ 3 - b ^ 3 → ¬ q ∣ c - b → ¬ q ^ 2 ∣ S0_nat c b

これを作って、定理 FLT_d3_by_padicValNat に渡せば、証明できます。

難しい理論はたぶん使ってない！

その仮定を作り出すためのフィルター補題定理群が完成したという話です。
つまりは…。たぶん。証明完了した。
（但し、３乗関連の３倍数を取り除いた数の集合において言える。くらい）

まあ、現在黙々と一人で検証中だけど。
宇宙式が一応、功を奏した結果として。

リポジトリ (nightly) で、公開中

考察

なんか、判定テスト定理として出来上がった FLT_d3_by_padicValNat ですが内部では GN 使って判定しているので n = 3 以外も素数 p で判定できる定理になるだろうということで一般化も可能な領域に居る。

その際に、仮定が一般化されるので、あらゆる仮定構築で遊べるのではないでしょうか？？という話。

sorry は残ってない。Mathlib.FLT を直接利用してないので、MkMath 内の補題を解析すれば別視点での FLT の構造が解るかもしれない。というところ。

本格的に数学詳しくないので、もうこれ以上は数学に人生かけている人に、任せようかな。まあ、興味ある人で人生時間に余裕がある人は突っ込め！

仮定の構築の解説を note で書こうと思ったけど、他の研究もあるので、
（どんどん出てきてしまう）GitHub に *.md で、議論ログがちらほら落ちてるから拾って読んでください。

2026/02/24 17:04

D.

#FLT #フェルマーの最終定理 #仮定式 #仮定 #補題 #定理 #Lean #Lean4 #Mathlib #Mathlib4 #宇宙式 #無次元宇宙式 #GitHub #リポジトリ #nightly
#padicValNat #Markdown #議事録 #議論ログ #証明 #形式化証明

Appendix

FLT n=3 判定のための定理

-- ========================================
-- § 3. 矛盾導出（層A + 層B統合）
-- ========================================

/-- **メイン定理：別解による FLT d=3 証明**

Zsigmondy原始素因子 + padicValNat評価による背理法：
平方自由性仮定の下で、完全3乗仮定と矛盾を導出。

**入力（仮定）:**
- `ha : 0 < a`, `hb : 0 < b`, `hc : 0 < c` - 正の整数
- `hab : Nat.Coprime a b` - a と b は互いに素
- `hS0_not_sq : ∀ {q : ℕ}, Nat.Prime q → q ∣ c^3 - b^3 → ¬ q ∣ c - b → ¬ q² ∣ S0_nat c b`
  - 相対多角数S0(c,b) = c²+cb+b² は各原始素因子 q に対して平方自由
  - すなわち：q が c³-b³ を割り、かつ q が (c-b) を割らない任意の素数 q について、
    q² は S0(c,b) を割らない

**証明戦略（層統合）:**

1. **層A（Zsigmondy原始素因子）**
   - 存在補題により、q | (c³-b³) かつ ¬ q | (c-b) を満たす素数 q が存在

2. **層B（padicValNat上界）**
   - 仮定 hS0_not_sq から ¬ q² ∣ S0(c,b)
   - padicValNat上界：v_q(c³-b³) ≤ 1

3. **矛盾導出**
   - 完全3乗仮定：q | a より v_q(a³-b³) ≥ 3
   - 層B下界：v_q(c³-b³) = v_q(a³-b³)（cube_sub_eq_of_add_eq より）
   - 矛盾：3 ≤ v_q(c³-b³) ≤ 1

**出力（結論):**
`a³ + b³ ≠ c³`（FLT d=3）
-/
theorem FLT_d3_by_padicValNat {a b c : ℕ}
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
    (hab : Nat.Coprime a b)
    (hS0_not_sq :
      ∀ {q : ℕ}, Nat.Prime q → q ∣ c ^ 3 - b ^ 3 → ¬ q ∣ c - b → ¬ q ^ 2 ∣ S0_nat c b) :
    a ^ 3 + b ^ 3 ≠ c ^ 3 := by
  intro h_eq

  have hcop_cb : Nat.Coprime c b := coprime_cb_of_eq hab h_eq
  have hbc : b < c := by
    by_contra hbc_not
    have hcb : c ≤ b := Nat.not_lt.mp hbc_not
    have hc3_le : c ^ 3 ≤ b ^ 3 := Nat.pow_le_pow_left hcb 3
    have hsum_le : a ^ 3 + b ^ 3 ≤ b ^ 3 := by simpa [h_eq] using hc3_le
    have ha3_pos : 0 < a ^ 3 := by positivity
    omega

  obtain ⟨q, hq_prime, hq_dvd_diff, hq_ndiv_diff⟩ :=
    exists_prime_factor_cube_diff hbc hb hcop_cb

  have hsub : c ^ 3 - b ^ 3 = a ^ 3 := cube_sub_eq_of_add_eq h_eq
  have hq_dvd_a3 : q ∣ a ^ 3 := by simpa [hsub] using hq_dvd_diff
  have hq_dvd_a : q ∣ a := hq_prime.dvd_of_dvd_pow hq_dvd_a3

  have h_lower_a3 : 3 ≤ padicValNat q (a ^ 3) :=
    padicValNat_lower_bound_of_dvd_d3 ha hq_prime hq_dvd_a
  have h_lower : 3 ≤ padicValNat q (c ^ 3 - b ^ 3) := by
    simpa [hsub] using h_lower_a3

  have h_upper : padicValNat q (c ^ 3 - b ^ 3) ≤ 1 :=
    padicValNat_upper_bound_d3 hbc hc hb hq_prime hq_dvd_diff hq_ndiv_diff
      (hS0_not_sq hq_prime hq_dvd_diff hq_ndiv_diff)

  have : (3 : ℕ) ≤ 1 := le_trans h_lower h_upper
  omega

#print axioms FLT_d3_by_padicValNat  -- OK: 2026/02/24  6:27
-- 'DkMath.FLT.FLT_d3_by_padicValNat' depends on axioms: [propext, Classical.choice, Quot.sound]

利用例の直前補題

/--
`CounterexamplePattern.classifyLift` を経由して `hS0_not_sq` を供給する版。
-/
theorem FLT_d3_by_padicValNat_of_classifyLift {a b c : ℕ}
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
    (hab : Nat.Coprime a b)
    (hClassify :
      ∀ {q : ℕ}, Nat.Prime q → q ∣ c ^ 3 - b ^ 3 → ¬ q ∣ c - b →
        classifyLift ({ c := c, b := b, q := q } : CounterexampleInput) = LiftStatus.impossible) :
    a ^ 3 + b ^ 3 ≠ c ^ 3 := by
  apply FLT_d3_by_padicValNat ha hb hc hab
  intro q hq hq_dvd_diff hq_ndiv_diff
  let x : CounterexampleInput := { c := c, b := b, q := q }
  have hprim : primitivePrimeGate x := by
    exact ⟨hq, hq_dvd_diff, hq_ndiv_diff⟩
  have hcls : classifyLift x = LiftStatus.impossible := by
    simpa [x] using hClassify hq hq_dvd_diff hq_ndiv_diff
  have hnosq : noSquareGate x :=
    noSquareGate_of_classifyLift_impossible hprim hcls
  simpa [x, noSquareGate] using hnosq

#print axioms FLT_d3_by_padicValNat  -- OK: 2026/02/23 12:08
-- 'DkMath.FLT.FLT_d3_by_padicValNat' depends on axioms: [propext, Classical.choice, Quot.sound]

それで使ってる補題

/--
反例抽出器の最小判定器。

- `primitivePrimeGate` が閉じない場合は `undecided`
- 閉じていて `noSquareGate` が成り立つなら `impossible`
- 閉じていて `noSquareGate` が崩れるなら `possible`
-/
noncomputable def classifyLift (x : CounterexampleInput) : LiftStatus := by
  classical
  exact if hexc : exceptionalPhaseGate x then
    LiftStatus.undecided
  else if hprim : primitivePrimeGate x then
    if hnosq : noSquareGate x then LiftStatus.impossible else LiftStatus.possible
  else
    LiftStatus.undecided

と、言う感じで辿ってください。