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

バグを取っ掛かりにした証明と予想。

他の環境では証明できなそう

これを信じない人は元の証明が間違ってることも期待してるの？

AIの証明結果を検証するのが
ますます大変になる。

その検証もＡＩで機械化
せねば。　そのレポートは
検証対象以上に膨大なレポートに
なるかも。

人間は、ＡＩに解けない問題を
与えて、結果だけを応用して
実用化する方向に行くかも。

真理かどうかは実用化できて
効果を産むかどうかになる。

LEANは帰納的定義でいろんな概念組み上げて証明作るんだから
ある意味無限降下法よ

>>74
現場猫理屈？やん
役立つから真理でヨシ！ｗ