Dukungan AI Menjadi Hal Biasa di Situs Soal Erdős

• 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

[GN⁺]

Komentar Hacker News

• Sungguh pengalaman yang menakjubkan bahwa kita bisa melempar paper ML yang berpusat pada matematika ke asisten AI lalu menerima penjelasan sederhana atau pseudocode
  Bagi saya, yang sudah lebih dari 25 tahun tidak pernah memakai hal yang dipelajari di universitas, ini benar-benar sangat membantu

  • Saya penasaran bagaimana memverifikasi apakah penjelasan itu akurat. Definisi matematis punya banyak bagian yang sangat subtil
  • Menurut saya, justru di sinilah LLM paling bersinar untuk pembelajaran
    Kita bisa memasukkan paper ke Claude, mendapatkan gambaran besarnya, lalu melanjutkan dengan pertanyaan-pertanyaan
    Bahkan di bidang seperti biologi yang tidak saya pelajari saat S1 atau S2, saya bisa menggali lebih dalam seolah bercakap-cakap dengan tutor yang berpengetahuan
  • Notasi matematika sangat bergantung pada konteks, jadi jika meminta LLM mengubahnya ke bahasa berkonteks rendah seperti Lisp, kita bisa jauh lebih cepat memahami strukturnya

• Saya berharap para peneliti dan perusahaan mendapatkan lebih banyak peningkatan produktivitas dalam riset ilmiah
  Bahkan asisten yang tidak sempurna pun cukup mampu memberi leverage besar

  • Ada versi beta aplikasi formalization untuk iOS yang disebut Tao → Aristotle
    Katanya ini startup yang didirikan CEO Robin Hood

• 'Vibe formalizing' terasa seperti perpanjangan logis dari 'vibe engineering' dan 'vibe coding'
  Saat potongan-potongan masalah tidak pas dengan baik, pendekatan seperti 'Move 37 as a Service' yang menggabungkan metode informal dan ketelitian matematis terasa menarik

  • Dulu saya pernah tersendat saat membaca paper polyhedral compilation, dan ChatGPT membantu memandu proses reasoning dengan baik
    Tentu ada bagian yang salah, tetapi lewat percakapan yang mencerminkan kebingungan saya, saya bisa memperdalam pemahaman
    AI sangat kuat khususnya dalam menangkap titik kebingungan pengguna

• Saya mendengar cerita tentang cara melafalkan nama matematikawan Hungaria Erdős
  Dalam bahasa Hungaria, ejaan dan pelafalan hampir selalu cocok, tetapi untuk nama ada pengecualian
  Dalam bahasa Inggris kira-kira terdengar seperti “airdish”

  • Ő hanyalah bunyi œ(oe). Akhiran -y pada nama Hungaria adalah jejak dari akhiran -i yang dulu menandakan garis keturunan bangsawan
    Contoh: Görgey, Széchényi, Lánczos, dll.
    Urutan nama Hungaria seperti Jepang, yaitu urutan nama keluarga-nama depan (big endian). Contoh: “Erdős Pál”, “Neumann János”
  • Ada puisi humor yang saya lihat di papan pengumuman jurusan matematika tahun 1960-an — leluconnya adalah paper karya Erdos membantah teorema bahwa lingkaran itu bulat
  • Karena makna tanda pelafalan (diakritik) berbeda di tiap bahasa, menurut saya terasa janggal jika tanda ala Hungaria dipakai mentah-mentah dalam kalimat bahasa Inggris
  • Awalnya pelafalan “airdish” terasa aneh, tetapi ketika akhiran ‘os’ dipalatalisasi, bunyinya jadi cukup masuk akal
  • Mungkin karena saya bukan orang Amerika, sepertinya tidak ada yang terlalu peduli dengan soal pelafalan seperti ini

• Menarik bahwa di komentar ada reaksi yang bernuansa anti-Lean

  • Saya bukan matematikawan, tetapi saya penasaran apakah materi anti-Lean itu dapat dipercaya
    Saya ingin tahu apakah itu sekadar mempromosikan pendekatan lain, atau memang secara filosofis menentang Lean
  • Tokoh terkenal seperti Tao memang cenderung menarik perhatian orang eksentrik atau penganut teori konspirasi

• Hasil memakai AI dalam matematika riset terasa campur aduk
  Kadang ia bisa melengkapi argumen nontrivial secara otomatis, tetapi di area tertentu ia benar-benar tersesat
  Untuk saat ini, saya rasa AI masih berguna hanya sebagai alat bantu, bukan pengganti matematikawan

  • Saya juga punya pengalaman serupa. Saya pernah memberinya masalah perhitungan permutasi sederhana dari sebuah paper, dan justru memakan waktu lebih lama daripada mengerjakannya sendiri
    Dalam coding juga ada kalanya ia gagal menangkap bug sepele, tetapi pada pekerjaan yang kompleks sangat membantu
    Pada akhirnya, alat-alat ini masih jauh dari mampu menggantikan pakar, dan hype berlebihan justru bisa merusak kepercayaan
    Seperti ungkapan 'kalau menjanjikan bulan, ya harus memberi bulan', ekspektasi yang realistis itu penting

• Sulit dipercaya bahwa dalam hidup saya akan datang era seperti Star Trek di mana kita bisa berkata, “Komputer, gambarkan pembuktian untuk soal matematika ini”
  Andai “Beam me up Scotty” juga bisa dilakukan

  • Tapi kalau setiap kali begitu kita bisa mati, sepertinya itu agak merepotkan

• Malam ini saat menyetir saya berbicara dengan ChatGPT tentang struktur rinci pipeline scheduler LLVM dan GCC
  Berkat itu produktivitas saya naik banyak, dan catatan terkait compiler yang sedang saya eksperimenkan bisa dirapikan otomatis
  Dulu ini hal yang bahkan tak terpikirkan

  • Menurut pengalaman saya, kemungkinan besar LLM salah pada sebagian detail
    Tentu hasilnya bisa berbeda untuk tiap orang

• Kalau AI diberi nama Erdos, rasanya Erdos number kita semua akan jadi 1

  • Atau terasa seperti penerus dari DR-DOS
  • Memang ada produk bernama Erdos, yaitu IDE terintegrasi AI

• Mengesankan bahwa ia memanfaatkan alat frontier yang sudah ada dengan baik untuk menciptakan lingkungan riset matematika yang kolaboratif

  • Untungnya, matematika adalah bidang di mana pengkultusan atau kontes popularitas tidak menentukan benar-salahnya hasil
    Karena itu, saya merasa matematika masih merupakan bidang langka yang bebas dari pengaruh pseudosaintifik