【AI】Claudeがフェルマーの最終定理を11日で形式化、1300万行のLeanコードで初の完全な機械検証済み証明を完成 [すらいむ★]

>>51
>無限降下法の適用限界を見誤ったと思われる
そういう意見よく見るんだけど、n=4のときの反例は(x^2)^2+(y^2)^2=(z^2)^2だからx^2,y^2,z^2がピタゴラス数になるという性質をふんだんに利用していて、無限降下法の適用限界も何も、そもそも他のnの証明でn=4のときのような無限降下法に持ち込めそうな気がしない。
何をどう見誤ったというんだろう

それはさておき、フェルマーはn=4の証明のあとにn=3の証明に取り掛かっていた形跡があるようで、本当に一般のn>2で証明していたなら個別にn=3の証明に手を出す理由がない。本人もn=4以外の証明はできていないことに気付いていたんだろうね

> 1300万行のLeanコード

確かに余白が足りなさそう

私は素晴らしい証明を生成できたが、それを書き出すには今のSSDは高すぎて容量が足らない。

ポアンカレ予想も形式化されたらしい(470万行)
次はABC予想?

ヒルベルトが聞いたらびっくりするだろな。まさか形式論理が現実に実用化されるなんて思ってなかったというだろうと思う。

ヒルベルトは形式主義派だったので何の驚きもないはず
ペアノの公理を拡張していけばいいと思っていたわけだし
証明は有限な手順に抑え込めると考えていた
むしろ完全勝利という感じだろう
計算機数学の方の論理主義の隆盛の方が驚きだろう
あと直観主義で証明できる数学範囲が意外に多いことにも驚いてるはず

数学がいう有限でできるということと、それが現実に実行できるということの間には大きな隔たりがある。
ゲームの理論から、囲碁が先手必勝であるか後手必勝であるか必ず引き分けに持ち込めるかの3通りだとして、
それのどれであるかを決定するのは大変で、厳密な証明はまず無理だろう。囲碁までいかずとも、8ｘ8盤の
オセロが先手必勝か後手必勝か必ず引き分けにできるかのどれかを決定することは人力では無理。
＃もしもある命題の証明が存在してそれを有限長の記号の列で記述が可能であるとすれば、
「有限の手数」で必ずその記号の列を具体的に割り出すことが機械的にできるが、
それは現実的には到底無理な話だ。
また、もしも「ある命題の証明が存在しない」ことの証明が存在していて
それを有限長の記号の列で記述できるのだとすれば、
その記述もまた有限の手数で見いだせることになるが、
もちろんこれも現実的には到底実行することは無理だ。
有限だといっても場合の数が多すぎるので。

有限の立場をまるで理解できてない

>>83
先進文明は次世代AIみたいな物を開発してそれのおかげで地球人には未知の法則の発見も含めかなり先に行ってるはず
我々がコンピュータを駆使して昔の人が手計算では到底出来なかったことを日々しているのと同じ

形式化ってどういうこと？

>>96
オセロは引き分けという結論が出たでしょ

オセロは引き分け、を示すことは人力では無理だろ。