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

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

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

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

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

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

正否の決定が不能な命題をAIに証明をさせようと試みたら何が起こるだろうか？
AIは証明を延々と探し求めるだけだろうか？それとも探索の過程でその命題は
決定不能なものであることを証明できるのだろうか？

ある体系の中での証明不能性はメタの議論になるのが普通だから、一段階高い立場を要するだろうな。