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

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

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

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

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

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