OpenAI terbitkan 722 manuskrip matematika hasil AI

OpenAI merilis sekumpulan besar hasil matematika yang ditulis oleh model internal yang belum dirilis, memublikasikan 722 manuskrip yang dikelompokkan ke dalam 372 famili di GitHub. Satu famili mengumpulkan sebuah hasil utama beserta argumen pendukung dan bukti alternatifnya. Menurut README, setiap hasil rata-rata memakai sekitar tiga jam thinking compute ChatGPT Pro, dan model diberi sekitar 4.000 soal selama evaluasi. Topiknya adalah matematika riset sungguhan, bukan sekadar latihan: eksponen irasionalitas pi, konjektur direct-finiteness Kaplansky pada karakteristik dua, formula Mezard-Parisi untuk diluted spin glass, dan masalah isomorfisme untuk free group factor, di antaranya.

Bagian yang jujur ada pada catatan peringatannya. Tidak semua hasil sudah diverifikasi formal. OpenAI menyertakan pustaka Lean dengan formalisasi terverifikasi mesin untuk sebagian pekerjaan, tetapi README menyatakan terus terang bahwa sebagian hasil yang belum diformalkan bisa saja bermasalah. Hal ini penting karena klaim matematika AI sebelumnya tahun ini, termasuk pembantahan konjektur Erdos berusia 80 tahun pada Mei, menuai pujian sekaligus kritik tajam dari para matematikawan soal apakah argumennya benar-benar kuat. Dengan menerbitkan manuskrip mentah dan berkas Lean, komunitas bisa memeriksa langsung, bukan sekadar percaya pada ringkasan pers.

Kenapa ini penting

Kalau Anda bekerja di bidang matematika atau formal verification, ini adalah dataset yang benar-benar bisa diaudit: 722 argumen dengan formalisasi Lean parsial, dirilis untuk diperiksa, bukan sekadar diumumkan. Pertanyaan terbukanya adalah berapa banyak yang bertahan setelah ditinjau, dan OpenAI mempersilakan Anda membuktikannya sendiri.