HN5311
数学界の難問、フェルマーの最終定理がLean 4でついに証明！
Fermat's Last Theorem in Lean 4
aaraujo002・約10時間前
議論
7件Lean 4を用いてフェルマーの最終定理（Fermat's Last Theorem）が証明されました。定理証明支援系を用いた数学の形式化において、大きなマイルストーンとなる出来事です。
俺のほうがずっと短いんだけどな…
ついにフェルマーが余白に書き残そうとしたものが手に入ったな: aa2d8b34692b16c70f699536de0d8e75b9a3e9ef
すごく印象的な成果だね。チームのみんなに拍手。
Leanのコードの一部が、既存のLeanライブラリにコントリビュートできるような形になっているか気になる。Fableに他人が扱えるような形式化ライブラリ向けのきれいなコードを書かせるには、かなりの手作業が必要になるというのが俺の経験則。でも、これだけの前提条件が形式化されているわけだし、一つの卒業研究的な証明のためだけに終わらせてしまうのはもったいないよね！（以前のコメントの再掲だけど、こっちの方が文脈に合う気がする）
「grind（やり込み/地道な作業）」がキーワードになってるの最高だな。