Para matematikawan menanggapi kemajuan terbaru AI dalam pembuktian teorema dengan campuran antusiasme dan frustrasi. Sebagian penggemar AI berpendapat bahwa saatnya telah tiba untuk memformalkan seluruh matematika sebagai warisan bagi generasi mendatang. Para penulis, sekelompok pakar formalisasi yang mencakup Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, dan Adam Topaz, mengatakan bahwa mereka bersimpati pada usulan tersebut dan optimistis terhadap peran AI. Namun, mereka sangat prihatin dengan seruan untuk memformalkan segalanya secepat mungkin.
Jika dilakukan dengan baik, upaya formalisasi berskala besar dan terkoordinasi dapat sangat memperluas eksplorasi dan penemuan matematika. Jika dilakukan dengan buruk, para penulis memperingatkan, upaya itu paling baik hanya akan menjadi pemborosan sumber daya dan paling buruk dapat menimbulkan kerusakan jangka panjang. Mereka menegaskan bahwa pandangan yang disampaikan adalah pandangan pribadi mereka dan bukan pandangan organisasi mana pun tempat mereka berafiliasi, serta bahwa rekan-rekan mereka memiliki beragam opini tentang formalisasi berbasis AI.
Para penulis menunjuk contoh-contoh terbaru. Sebuah proyek untuk memformalkan hasil Maryna Viazovska tentang pengemasan bola terganggu ketika sebuah perusahaan AI mencoba mengambil alihnya. Tim asli mendapati bahwa membersihkan kode yang dihasilkan AI lebih merepotkan daripada manfaatnya, sehingga mereka membuangnya dan membangun ulang pekerjaan itu dengan benar, dengan bantuan AI. Demikian pula, ketika Anthropic mengumumkan bahwa Claude telah memverifikasi secara formal Teorema Terakhir Fermat dalam 13 juta baris kode, hasilnya mengesankan namun nilai berkelanjutannya terbatas, karena teorema tersebut tidak pernah benar-benar diragukan.
Poin utamanya adalah bahwa artefak formal hanya bernilai jika orang menggunakannya. Formalisasi penting karena apa yang memungkinkannya di luar sekadar kebenaran, seperti mengeksplorasi generalisasi, menghubungkan cabang-cabang matematika, dan memperhalus konsep. Para penulis berargumen bahwa pemahaman yang sesungguhnya, bukan semata jumlah kode yang terverifikasi, yang seharusnya memandu upaya ini.
Sumber: Hacker News · Diringkas oleh HeadlinesBriefing