- Dalam proses penyelesaian soal Erdős #367, alat AI memainkan peran kunci, dan dilaporkan ada contoh kolaborasi dengan matematikawan manusia
- Wouter van Doorn mengajukan kontra-contoh buatan manusia untuk bagian kedua soal, lalu Gemini Deepthink menghasilkan pembuktian lengkap untuk kongruensi yang terkait
- Terence Tao memublikasikan versi yang lebih sederhana dari bukti berbasis teori bilangan aljabar p-adik milik Gemini, lalu menyebut kemungkinan formalisasi Lean
- Boris Alexeev menyelesaikan formalisasi Lean menggunakan alat Aristotle dari Harmonic, dan untuk mencegah penyalahgunaan AI, proposisi akhirnya diverifikasi secara manual
- Rangkaian proses ini menunjukkan bahwa bantuan AI dalam riset matematika secara bertahap menjadi prosedur standar
Contoh kolaborasi AI pada soal Erdős #367
- Pada 20 November, Wouter van Doorn mengajukan kontra-contoh untuk bagian kedua soal, yang bergantung pada asumsi bahwa suatu kongruensi tertentu benar
- Ia meminta peserta lain memverifikasi validitas kongruensi tersebut
- Beberapa jam kemudian, Terence Tao menyodorkan masalah ini ke Gemini Deepthink, dan dalam sekitar 10 menit memperoleh pembuktian lengkap untuk kongruensi itu sekaligus verifikasi seluruh argumen
- Bukti dari Gemini menggunakan teori bilangan aljabar p-adik, dan Tao mengubahnya menjadi bukti elementer yang lebih sederhana lalu memublikasikannya di situs
- Tao menyebut bahwa bukti ini kemungkinan bisa "divibe-formalkan" di Lean
Formalisasi dan verifikasi Lean
- Dua hari kemudian, Boris Alexeev menyelesaikan formalisasi Lean menggunakan alat Aristotle dari Harmonic
- Untuk mencegah penyalahgunaan AI, proposisi akhirnya diformalkan sendiri secara manual
- Seluruh proses memakan waktu sekitar 2–3 jam, dan hasilnya dipublikasikan secara online
- Tao kemudian menggunakan AI untuk penelusuran literatur, tetapi meski ada beberapa riset terkait, tidak ditemukan yang berhubungan langsung dengan soal #367
Reaksi dan diskusi komunitas
- Sebagian pengguna mengikuti pembaruan Tao dengan minat, sebagai gambaran kondisi pemanfaatan AI dalam matematika akademik
- Pengguna lain menyampaikan pandangan kritis terhadap pendekatan formalis Lean, dengan menilai bahwa pemahaman matematika adalah kompresi, sedangkan Lean memecahnya menjadi dekompresi ke detail tingkat rendah
- Dokumen terkait “Against Lean: Why Proof Assistants Formalize the Wrong Thing” berargumen bahwa Lean dan pembantu bukti serupa salah menangkap hakikat matematika
- Pengguna lain lagi menyinggung masalah akurasi dalam percakapan AI, sambil menilai bahwa penggunaannya menyenangkan meski memerlukan penyesuaian yang teliti
Belum ada komentar.