Matematikawan Menolak Terobosan Konjektur OpenAI dalam 24 Jam: 'AI Membuktikan Setiap Kalimat, tapi Ini Bukan Lagi tentang Konjektur Asli'

OpenAI mengklaim bahwa model AI generasi terbarunya memecahkan sepuluh masalah matematika kelas dunia, termasuk membuktikan salah konjektur kekakuan Connes. Keesokan harinya, seorang matematikawan manusia menanggapi dengan makalah yang berargumen bahwa contoh penyangkal AI tersebut tidak valid. Penulisnya, J. L. Nielsen dari Pusat Fisika Topologi di Universitas Kansas, menelusuri 37.000 baris kode Lean 4 OpenAI dari awal hingga akhir, memetakan setiap objek kembali ke prototipe matematikanya, dan mengidentifikasi dua jalur kegagalan yang independen. Konjektur kekakuan Connes menyatakan bahwa jika dua grup memiliki struktur aljabar terkait yang sama dan memenuhi dua kondisi tambahan (ICC dan properti Kazhdan (T)), maka grup-grup tersebut harus isomorfik. Model OpenAI mengonstruksi dua grup yang tidak isomorfik yang menghasilkan aljabar yang sama, dengan bukti bahwa kedua grup memenuhi ICC dan properti (T). Nielsen menunjukkan bahwa salah satu grup yang dikonstruksi AI sebenarnya tidak memenuhi kondisi tambahan, karena tidak memiliki ICC maupun properti (T). Dia mencantumkan tiga kemungkinan alasan: representasi properti (T) dalam kode tidak sesuai dengan definisi asli Kazhdan; bukti hanya berlaku untuk sebagian grup tetapi diterapkan pada keseluruhan; atau grup dalam kode bukanlah yang dijelaskan dalam dokumen penjelas. Nielsen juga melakukan pemeriksaan baris demi baris pada kode, membuat tabel referensi silang yang mencantumkan nama setiap objek matematika dan nomor barisnya. Dia menemukan bahwa lemma yang digunakan untuk membuktikan ICC diterapkan pada objek setelah transformasi ganda, bukan pada grup asli dengan elemen sentralnya, sehingga tidak secara langsung mencakup elemen-elemen kritis. Dia menulis dua sanggahannya sebagai kode Lean dan mengompilasinya menggunakan Lean 4.32.2. Bagian akhir makalah membahas konteks yang lebih luas: kernel Lean memastikan kebenaran formal, tetapi tidak memastikan apakah pernyataan tersebut benar-benar membuktikan kesimpulan yang dimaksud. Mengutip Terence Tao, memverifikasi bukti memeriksa pernyataan formal itu sendiri, bukan kesesuaiannya dengan maksud, sehingga tinjauan manusia tidak dapat digantikan. Audit masa lalu terhadap lima tolok ukur Lean yang umum menemukan 4.833 masalah, termasuk contoh penyangkal, teorema kosong, dan aksioma yang tidak dapat diandalkan, semuanya terverifikasi mesin, dengan manusia kemudian mengonstruksi contoh penyangkal untuk menunjukkan bahwa pernyataan yang terbukti adalah salah. Nielsen menulis bahwa formalisasi OpenAI mungkin telah menetapkan dengan benar setiap kesimpulan yang diklaimnya, tetapi apa yang tidak ditetapkannya—dan apa yang tidak dapat diperiksa oleh kernel Lean—adalah apakah kesimpulan-kesimpulan ini terkait dengan kata-kata asli konjektur. Konjektur kekakuan Connes tetap terbuka.