数学者がOpenAIの予想突破を24時間以内に否定：「AIはすべての文を証明したが、もはや元の予想ではない」

OpenAIは、次世代AIモデルが、Connes剛性予想の反証を含む、世界クラスの数学問題10問を解いたと主張した。その翌日、人間の数学者が、AIの反例は無効であると論じる論文で応答した。カンザス大学トポロジー物理学センターのJ. L. Nielsen氏は、OpenAIのLean 4コード37,000行を最初から最後まで追跡し、各オブジェクトを数学的なプロトタイプにマッピングし、2つの独立した失敗経路を特定した。Connes剛性予想は、2つの群が同じ関連する代数構造を持ち、2つの追加条件（ICCとKazhdanの性質(T)）を満たす場合、それらの群は同型でなければならないと述べている。OpenAIのモデルは、同じ代数を生成する2つの非同型群を構築し、両方の群がICCと性質(T)を満たすという証明を提供した。Nielsen氏は、AIが構築した群の1つが実際には追加条件を満たしておらず、ICCでも性質(T)でもないことを指摘した。彼女は、コードの性質(T)の表現がKazhdanの元の定義に忠実に対応していない、証明が群の一部にのみ当てはまるが全体に適用された、またはコード内の群が説明文書が説明するものとは異なる、という3つの可能性を挙げた。Nielsen氏はまた、コードを1行ずつチェックし、各数学的オブジェクトの名前と行番号を相互参照表にリストした。彼女は、ICCを証明するために使用された補題が、双対変換後のオブジェクトに適用され、中心要素を持つ元の群には適用されなかったため、重要な要素を直接カバーしていないことを発見した。彼女は自分の2つの反論をLeanコードとして書き、Lean 4.32.2でコンパイルした。論文の最後のセクションでは、より広い文脈について論じている。Leanカーネルは形式的な正しさを保証するが、ステートメントが意図した結論を実際に証明しているかどうかは保証しない。テレンス・タオを引用すると、証明の検証は形式的なステートメント自体をチェックするものであり、意図との整合性をチェックするものではないため、人間によるレビューは置き換えられない。一般的なLeanベンチマーク5つの過去の監査では、反例、空の定理、信頼できない公理を含む4,833の問題が見つかり、すべて機械で検証され、後に人間が反例を構築して証明されたステートメントが偽であることを示した。Nielsen氏は、OpenAIの形式化は、それが主張するすべての結論を正しく確立したかもしれないが、確立しなかったこと、そしてLeanカーネルがチェックできないことは、これらの結論が元の予想の文言と関連しているかどうかであると書いた。Connes剛性予想は未解決のままである。