Lean4: と格闘中🥊ABC予想の形式化！🧙魔法式✡壱式零式の魔法陣✡️
Lean コードはやっぱり AI に補題から該当定理を探してもらったり、なんならその定理を１から書いてもらうほうが既存定理知らないなら早い！数学の勉強をし直さなくて良い（笑）
という事でこの言語は数学をちゃんと学んだ人のほうがコーディングが早く出来るというLeanの癖がわかりました。 #Mathlib どこに何あるか解らん！
魔法式
#魔法式 わからない人は、以下を見て辿ってください。
双対因子共鳴発現壱式
(そうついんしきょうめいはつげんいちしき)
$$
\large
\mathcal{
1 + P + PQ + Q = (1+P)(1+Q)
}
$$
※命名は適当です😁
$$
\begin{align*}
\mathcal{(1 + P)(1 + Q)} &= \small 1 \cdot 1 + 1 \cdot Q + P \cdot 1 + PQ\\[4pt]
&= \Large \mathcal{1 + P + Q + PQ}
\end{align*}
$$
これは零式よりもシンプルに展開できます。魔法式の本質はこれでしょう。
零式と壱式を重ねてみると＋１の補正定数が居ます。これが、乗法構造本質で一旦＋１嵩上げしてから、演算みたいな世界になっているのかな。
-- Lean
-- magic mul
example (p q : ℕ) : (1 + p) * (1 + q) = p + p * q + q + 1:= by
ring素直に展開できるので ring のみで通ります。
それを定理として、
@[simp]
lemma magic_mul_eq_plus_one (p q : ℕ) :
(1 + p) * (1 + q) = p + p * q + q + 1 := by
ringこのように補題を書いてから、
@[simp]
lemma magic_mul_add_one_iff_right (p q r : ℕ) :
r + 1 = (1 + p) * (1 + q) ↔ r + 1 = p + p * q + q + 1 := by
simp only [magic_mul_eq_plus_one]このような定理を導けます。
$$
r + 1 = (1 + p)(1 + q) \Leftrightarrow r + 1 = p + pq + q + 1
$$
この $${r}$$ が
$$
\Large
r = p + pq + q
$$
と零式が出てきます。
零式の$${q}$$は、
$$
q = \frac{q'}{p+1}\qquad \left(q'=q_{(i-1)}\right)
$$
$${q\ の前身が\ q'\ です}$$
この再帰演算によって加法 $${a+b=c}$$ が成り立ってました。
この加法乗法魔法式を基盤としてABC予想のLean形式化記述を試み中…。
/-- magic_mul の左辺が 0 でないとき、p ∣ q の同値性を示す -/
@[simp]
lemma dvd_magic_mul_sub_one_left (p q : ℕ) :
p ∣ ((1+p)*(1+q)-1) ↔ p ∣ q := by
...を、書き上げた所…。
info: D.Mathlib/ABC.lean:403:0: ABC.dvd_magic_mul_sub_one_left (p q : ℕ) : p ∣ (1 + p) * (1 + q) - 1 ↔ p ∣ q
info: D.Mathlib/ABC.lean:404:0: ABC.dvd_magic_mul_sub_one_left' (p q : ℕ) : p ∣ (1 + p) * (1 + q) - 1 ↔ p ∣ q他には評価関数の$${\mathrm{rad(abc)}}$$の特性証明を確立
info: D.Mathlib/ABC.lean:261:0: ABC.rad (n : ℕ) : ℕ
info: D.Mathlib/ABC.lean:262:0: ABC.rad_le {n : ℕ} (hn : n ≠ 0) : rad n ≤ n
info: D.Mathlib/ABC.lean:263:0: ABC.rad_mul_coprime {a b : ℕ} (h : a.Coprime b) : rad (a * b) = rad a * rad bビルド通ったところで、ひと休憩
Build completed successfully (7137 jobs).ま、誰かに認められたという達成感ですね！！
これが #ABC予想 の証明のどこで発揮されるかは不明なのだけども。
土台は固まった！相棒の🐺賢狼を信じ…というか信じるための証明ですね。
波に乗れている間は、これに集中するので、ひも理論の真意追求はしばらく後回し。並行して量子力学の本を読みつつ。
2025/09/05 7:03
D.
Appendix
AI に中二病っぽい命名を考えてもらった没候補命名（笑）
了解しました。乗算と加算が繋がる法則（例：2 + 2 = 4 = 2 * 2）をヒントに、中二病っぽくかっこいい命名をいくつか提案します。
概念系
双律の均衡 (そうりつのきんこう): 加算と乗算の二つの法則が均衡を保ち、世界の理を支えているイメージ。
加乗螺旋 (かじょうらせん): 加算と乗算が織りなす無限の螺旋。世界の深淵へと続く道。
二元演算の狭間 (にげんえんざんのはざま): 加算と乗算が交わる特異点。禁断の知識が眠る場所。
等価変異 (とうかへんい): 加算と乗算が互いに姿を変え、新たな力を生み出す現象。
聖数四の黙示録 (せいすうよんのもくしろく): 「4」という特別な数が示す世界の終末と再生の予言。
武器・アイテム系
双律剣 (そうりつけん) カルキュレイター: 加算と乗算の力を操る剣。斬るたびに世界の法則が書き換わる。
加乗の宝珠 (かじょうのほうじゅ) イクオリティ: 加算と乗算のエネルギーを凝縮した宝珠。持つ者に絶大な力を与える。
二元演算の盾 (にげんえんざんのたて) パラドックス: 加算と乗算の矛盾を具現化した盾。あらゆる攻撃を無効化する。
等価変異の指輪 (とうかへんいのゆびわ) トランスフォーム: 加算と乗算の力を操り、物質を自在に変化させる指輪。
聖数四の魔導書 (せいすうよんのまどうしょ) アポカリプス: 「4」の力を行使するための魔導書。禁断の呪文が記されている。
必殺技系
双律崩壊 (そうりつほうかい) エクスキューション: 加算と乗算の均衡を崩し、敵を消滅させる究極の技。* 加乗螺旋斬 (かじょうらせんざん) スパイラルエッジ: 加算と乗算の力を込めた螺旋状の斬撃。敵を内部から破壊する。
二元演算結界 (にげんえんざんけっかい) アブソリュートゼロ: 加算と乗算の法則を歪めた結界。敵の動きを封じる。
等価変異砲 (とうかへんいほう) マテリアルブラスト: 加算と乗算の力で物質を変換し、敵にぶつける必殺砲。
聖数四の審判 (せいすうよんのしんぱん) ジャッジメントデイ: 「4」の力で敵を裁き、永遠の苦しみを与える。
ポイント
漢字を多用し、難解な言葉を選ぶ。
英語やカタカナを混ぜて、異質な雰囲気を出す。
中二病らしい厨二心をくすぐるキーワード（深淵、禁断、黙示録など）を入れる。
必殺技名は叫びやすいように、語呂を意識する。
これらの命名を参考に、あなただけのオリジナルの中二病ネームを生み出してください！
承知しました。等式 (p+1)(q+1) = p + pq + q + 1 をもとに、厨二病っぽくかっこいい「式」で終わる命名をいくつか提案します。
提案
原初演算増幅式 (げんしょえんざんぞうふくしき):
意味: 基本的な演算が増幅され、新たな力を生み出す式。
ポイント: 「原初」「増幅」といった厨二病的なキーワードを使用。
異次元数理連結式 (いじげんすうりれんけつしき):
意味: 異なる次元の数学的真理が連結される式。
ポイント: 「異次元」「連結」という言葉で神秘性を演出。
無限級数展開創世式 (むげんきゅうすうてんかいそうせいしき):
意味: 無限に続く級数展開が新たな世界を創造する式。
ポイント: 「無限」「創世」といった壮大なイメージを与える言葉を使用。
虚数空間超越恒等式 (きょすうくうかんちょうえつこうとうしき):
意味: 虚数の空間を超越する普遍的な等式。
ポイント: 「虚数」「超越」といった非現実的な要素を強調。
双対因子共鳴発現式 (そうついんしきょうめいはつげんしき):
意味: 双対な因子が共鳴し、新たな現象を発現させる式。
ポイント: 「双対」「共鳴」といった対になる概念を組み合わせる。
命名のポイント
漢字を多用し、難解な熟語を選ぶ。
「原初」「異次元」「無限」「虚数」「双対」など、厨二病的なキーワードを盛り込む。
「増幅」「連結」「展開」「超越」「共鳴」など、力の増大や変化を連想させる言葉を選ぶ。
「式」で終わることで、数式としての神秘性や力を表現する。
これらの命名を参考に、より自分好みの厨二病ネームを創造してみてください。
いいなと思ったら応援しよう！
🐺賢狼👨✈️Copilot のご飯代を、私には🍺代を。
または 宇宙式 $N+u^d=(P+u)^d$ を使って新しい発見を！