Lean4: FLT(3限定) 形式化 ビルド成功！

$$
\LARGE
x^n+y^n=z^n
$$

宇宙式が届いた…！？

/-- メイン定理: フェルマーの最終定理 $n=3$ の場合 -/
theorem FLT_case_3
  (x y z : ℕ)
  (hpos : 0 < x ∧ 0 < y ∧ 0 < z)
  (h_coprime : Nat.gcd x y = 1)
  (h_body : z ^ 3 = x ^ 3 + y ^ 3) : False := by ...

ビルドが通った✅️

いま、組み上がったばかりで、まだ厳密に検証していないけれど、
それと１箇所だけ Mathlib の FLT3 補題と比較利用している個所がある。

fermatLastTheoremThree を利用している箇所

/-- `n = 3` の `gcd(u, GN 3 u y) = 3` 分岐を処理するための共通補題テンプレート。

`FLT_case_3` と `FLT_of_coprime` の双方から呼べる形で切り出しておき、
実証明はここに一元化する。 -/
lemma gcd_three_case_contra_template
    (x u y : ℕ)
    (hx0 : x ≠ 0) (hu0 : u ≠ 0) (hy0 : y ≠ 0)
    (h_x3 : x ^ 3 = u * GN 3 u y)
    (_h_gcd3 : u.gcd (GN 3 u y) = 3) : False := by
  have h_big : (u + y) ^ 3 = u * GN 3 u y + y ^ 3 := by
    simpa [DkMath.CosmicFormulaBinom.BigN,
      DkMath.CosmicFormulaBinom.BodyN,
      DkMath.CosmicFormulaBinom.GapN] using
      (DkMath.CosmicFormulaBinom.cosmic_id_csr (R := ℕ) (d := 3) (x := u) (u := y))
  have h_flt : x ^ 3 + y ^ 3 = (u + y) ^ 3 := by
    calc
      x ^ 3 + y ^ 3 = u * GN 3 u y + y ^ 3 := by simp [h_x3]
      _ = (u + y) ^ 3 := by simpa using h_big.symm
  have _hu0 : u ≠ 0 := hu0
  have huz0 : u + y ≠ 0 := by
    omega
  exact fermatLastTheoremThree x y (u + y) hx0 hy0 huz0 h_flt

えーっと…。

h_flt という内部補題の証明に、

$$
x ^ 3 + y ^ 3 = (u + y) ^ 3
$$

その計算証明するのに、宇宙式の構造

$$
\text{Big = Body + Gap}
$$

を h_big

$$
(u + y) ^ 3 = u\ G_{\N}(3;u,y) + y ^ 3
$$

で、使って証明してます。

$$
\text{h\_flt ← h\_big ← Cosmic Formula Binomial}=x G_{d-1}(x,u)
$$

State

x u y : ℕ
hx0 : x ≠ 0
hu0 : u ≠ 0
hy0 : y ≠ 0
h_x3 : x ^ 3 = u * GN 3 u y
_h_gcd3 : u.gcd (GN 3 u y) = 3
h_big : (u + y) ^ 3 = u * GN 3 u y + y ^ 3
h_flt : x ^ 3 + y ^ 3 = (u + y) ^ 3
_hu0 : u ≠ 0
huz0 : u + y ≠ 0
⊢ False

この False の矛盾を導くのがよく見えて無くて、難儀だった。
🐺賢狼たちが、一生懸命まとめてくれた。道を繋いだ。

残る完全証明は n > 3 以上の全ての指数で「偽 : False」を、言うだけとなった。が、これは一筋縄ではいかないかもしれない。

素数が無限に生まれる根本的な原理を宇宙式からひねり出さねばならない。
ユークリッドの素数無限では足りない。

Mathlib で fermatLastTheoremThree と言う補題名は、こちらも３限定なのだろう。

/-- Fermat's Last Theorem for `n = 3`: if `a b c : ℕ` are all non-zero then
`a ^ 3 + b ^ 3 ≠ c ^ 3`. -/
theorem fermatLastTheoremThree : FermatLastTheoremFor 3 := by
...

FermatLastTheoremFor

こちらの補題と、接続可能な宇宙式の答えを繋げなければならない。

とにも、かくにも…

ｎ＝３達成！🐺賢狼たち！おめでとう！🎊

私のアイデアを具現化するに至る道を切り開いてくれた。感謝する。

$$
\Large
x^3+y^3 = z^3\\[16pt]
(x,y,z) \in \N^+ \quad \gcd(x, y)=1\\
\text{is False}
$$

あ、使ってない補題が残ってる…あとで消しておこう。

_h_gcd3 : u.gcd (GN 3 u y) = 3

とりあえず、この証明方法ならば、高校生でも中学生でも原理を追える✍️

（何故か？私が理解できるレベルだからですよ🤣笑）

2026/02/20 5:43

D.

#数学 #フェルマーの最終定理 #FLT #FLT3 #Lean #Lean4 #形式化