Lean4: ABC予想の形式化 PR → nightly

３万行のソース分割、適当に終えて、最新 Lean でもビルドが通るように！

Lean は、リファクタリングがやりにくい！！！！💢

まだ nightly にマージしてないけど、とりあえず branch 公開して置いておく
そして、証明は「終わってない」のでご注意ください。

残ってるのは、なんかチェルノフとかの形式化を誰かがやってくれたら終わるみたいな話だったけど、それも怪しい！

$ cat *.lean | wc -l
28273

あ、足りない…ということは。ああ、そうか…。
ABC.lean 以降の after コードがまだ移行を終えてないのか…。

ぐぬぬ。

疲れた…。

2026/03/02 5:25

D.

#ABC予想 #Lean #形式化 #形式化証明
#GitHub #公開 #最新ニュース

Appendix

ニュース記事

有料記事なのだけど、並行して本家でもやってます。

2025年12月6日 10時00分

最近、この記事を再プッシュしていたので、note に貼り付けたソースコードを GitHub に上げることを、思い出したようにやりました。

2026年2月27日 5時00分

こっちの記事の表現も「決着がつくかもしれない。」
なので、決着ついてないのでしょう。有料部分読んでないのでわからん。

とりあえず私は、
証明になるかどうかわからん謎のコードの公開まではやった✍️無料だっ