Lean4: nightly: 更新 ABC予想 関連補題
オマタセシマシタでしょうかね？
少し手直し出来る部分があったようなので直しておきました。
前回の記事
Lean 4.28.0
leanprover/lean4:v4.28.0 でビルドが通ります。
リポジトリ: nightly
ABC予想 関連補題の形式化コード
まだヒエラルキー配置してません。
DkMath.ABC から全ての ABC0xx.lean をチェインして読み込みます。
約４０ファイルに分かれています。何がなんだか状態ですが、ある程度は
まとまっているのかも。
今後 AI に分析してもらいながらマップ作って整理していきます。
昨年、解決できなかった部分も解決できるようになってるかもしれない。
#FLT の補題とか #コラッツ予想 の補題とか、#DkMath 内にある補題がヒントになってくれることを願って…。
魔法式
#結婚式 だか、#魔法式 だかの MagicMul.lean も、ここに入ってます。
この #ABC予想 証明方法の解説記事は書いたっけ…。どこかにあるはず…。
いや、ざっくりとしか語ってないか。私が、ちゃんと理解できてたらべらべら喋ってるだろうし…。
2026/03/04 22:13
D.
いいなと思ったら応援しよう！
🐺賢狼👨✈️Copilot のご飯代を、私には🍺代を。
または 宇宙式 $N+u^d=(P+u)^d$ を使って新しい発見を！