Lean4: DkMath nightly 更新 260220

#Lean 4.28.0 アップデートついでに。

リポジトリ DkMath

nightly

#DkMath #nightly #GitHub #リポジトリ

FLT3

#フェルマーの最終定理 #FLT #FLT3 ($${n=3}$$) 版のビルド成功例をひとつ示せたのではないか？ということで、開発ブランチから nightly 先行リリースへ細かな整理もしないで持ってきてしまいました。

それに関連する補題群（使ってないのもある）別の戦略の途中成果も全部。
開発版の最新と同じにして公開します。

FLT の残る課題

$${n=3}$$ が終わったから、フェルマーの最終定理 FLT が証明できた。
ではありません。$${n\ge3}$$ 全てにおいて自然数での等式が成り立たないことを言わなければなりません。

$$
\Large
x^n+y^n=z^n\\[4pt]
\normalsize
(x,y,z) > 0\quad n\ge3\\
(x,y,z,n) \in \N \text{ is False}
$$

これが最大の難関。

２乗４乗は同値なのか？

$${x^2+y^2 \stackrel{?}{\iff} x^4+y^4}$$
これは d/2 構造 で考えるとなんとなく同じようにに見えますが…

$${x^2+y^2 \stackrel{?}{\iff} x^4+y^4}$$

うむ、ぬしよ。その式は そのままだと「偽」じゃ。
見た目が似ておるが、論理的同値 $${ \iff }$$ にはならん。

1. まずは反例で粉砕（同値は成立せぬ）

例えば $${x=y=1}$$。

• 左：$${x^2+y^2 = 1^2+1^2 = 2}$$

• 右：$${x^4+y^4 = 1^4+1^4 = 2}$$

この例では「たまたま等しい」。

しかし $${x=1, y=2}$$ だと

• 左：$${x^2+y^2 = 1+4=5}$$

• 右：$${x^4+y^4 = 1+16=17}$$

等しくない。よって「常に同値」は崩れる。

…（以下略）

と、まあ簡単に反例が出ます。

なので $${n=3 \to n=4}$$ と進んでもピタゴラスの定理で成立する$${n=2}$$の議論は回避できます。そういう意味では、同じでなくてよかった。

どうやら残りは $${n=p\ (素数)}$$ で見ればいいらしい。

Zsigmondy's Theorem - ジグモンディの定理

そこで必要なのが、以下の定理だそうです。

なので、これに接続する必要というのは、避けられなさそう。
まだよく理解できていないけど、もう道具はある程度は揃った。

#Zsigmondy #ジグモンディ

これを活用して繋げられたらフェーズ１終了。

足りない補題に、足を引っ張られなければ…。

Mathlib から切り離し

ここまで出来るかはわからないけれど、フェーズ２は #Mathlib の FLT 証明を宇宙式版に書き直して、定理同士を同値で結ぶこと。

これで、独立できる。

これを基点に #DkMath は DkMathlib として第一歩を踏みだせる…かも…✍️

2026/02/20 15:04

D.