Masalah Erdős #728 Hampir Diselesaikan Secara Otonom oleh AI

 (mathstodon.xyz)
2 poin oleh GN⁺ 2026-01-10 | 1 komentar | Bagikan ke WhatsApp
  • Masalah Erdős #728 baru-baru ini hampir diselesaikan secara otonom oleh alat AI, menandai tonggak baru dalam otomatisasi riset matematika
  • Masalah ini awalnya merupakan pertanyaan tentang faktorisasi prima koefisien binomial yang diajukan oleh Erdős, Graham, Ruzsa, Strauss pada 1975, dan lama tidak ditangani secara jelas karena syaratnya ambigu
  • ChatGPT menghasilkan pembuktian di bawah batasan yang telah disesuaikan, lalu Aristotle memformalkannya sebagai bukti formal Lean dan otomatis memperbaiki kesalahan
  • Setelah itu, beberapa peserta menulis ulang ke bahasa natural dengan bantuan ChatGPT dan berulang kali menyempurnakan versi yang memperkuat keterkaitan literatur serta struktur narasinya
  • Terence Tao menilai proses ini menunjukkan bahwa kemampuan AI untuk cepat menulis dan merevisi bukti berpotensi mengubah cara penulisan makalah riset itu sendiri

AI yang Menyelesaikan Masalah Erdős #728

  • Belakangan ini penerapan alat AI menunjukkan kemajuan baru dalam penyelesaian masalah Erdős, dan masalah #728 hampir diselesaikan secara otonom oleh AI
    • Setelah percobaan awal, versi yang direvisi dengan memasukkan umpan balik berhasil
    • Hasilnya tidak ditemukan kembali secara identik dalam literatur yang ada, hanya ada hasil serupa dengan pendekatan yang mirip
  • Kasus ini menunjukkan bahwa dalam beberapa bulan terakhir kemampuan AI menyelesaikan masalah matematika benar-benar meningkat
    • Di masa lalu juga ada contoh AI menyelesaikan masalah Erdős, tetapi kebanyakan kemudian ternyata sudah memiliki solusi dalam literatur
  • Untuk kasus ini, perumusan asli Erdős ternyata disajikan dalam bentuk yang keliru, dan baru belakangan direkonstruksi ke bentuk yang dimaksud
    • Ini menjelaskan mengapa riset terkait dalam literatur yang ada sangat terbatas

Sejarah Masalah dan Pendekatan Awal

  • Pada 1975, Erdős, Graham, Ruzsa, Strauss meneliti faktorisasi prima dari koefisien binomial (2n choose n) dan mengajukan beberapa masalah terkait
    • Salah satunya menanyakan apakah ada tak hingga banyaknya a, b, n yang memenuhi kondisi a!b! | n!(a+b−n)! dan a+b > n + C log n
    • Namun, beberapa bagian dijelaskan secara tidak jelas, termasuk besar kecilnya C
  • Beberapa bulan lalu, tim AlphaProof menemukan solusi sederhana untuk masalah ini, tetapi dianggap tidak sesuai dengan semangat masalah yang dimaksud, sehingga ditambahkan batasan a,b ≤ (1−ε)n
    • Setelah itu, pencarian literatur berbantuan AI juga hampir tidak menemukan riset terkait

Kolaborasi ChatGPT dan Aristotle

  • Pada 4 Januari, ChatGPT menghasilkan pembuktian untuk kasus C kecil di bawah batasan yang telah disesuaikan
    • Bukti ini kemudian diformalkan oleh Aristotle menjadi bukti formal Lean
    • Setelah naskah asli ditinjau ulang, terkonfirmasi bahwa makalah awal sebenarnya sudah membahas kasus C kecil
  • Peserta lain lalu mengubah bukti Lean menjadi bahasa natural dengan ChatGPT, dan melalui percakapan tambahan menyusun versi yang lebih baik
    • Versi ini menutup beberapa celah pembuktian, tetapi masih menyisakan gaya bahasa yang canggung khas AI dan kurangnya sitasi literatur
    • Meski demikian, hasilnya sudah mencapai tingkat keterbacaan yang cukup untuk memahami ide intinya

Penulisan Ulang Skala Besar dan Hasil yang Lebih Baik

  • Melalui prompt tambahan, ChatGPT menghasilkan pembuktian yang diperluas hingga kasus C besar
    • Ada beberapa kesalahan, tetapi Aristotle memperbaikinya secara otomatis dan menyelesaikan bukti yang tervalidasi Lean
  • Peserta ketiga lalu memadatkan bukti Lean, kemudian peserta lain melalui percakapan panjang dengan ChatGPT
    • menulis ulangnya menjadi bentuk makalah yang lebih matang dengan keterkaitan literatur dan struktur narasi yang lebih kuat
    • Hasil akhirnya dinilai lebih sedikit terasa seperti keluaran AI dan mendekati kualitas makalah riset
    • Tao menyebut teks ini telah ditinjau di forum masalah Erdős

Cara AI Mengubah Penulisan Makalah Riset

  • Tao menilai bahwa dalam makalah akhir, bagian inti tetap harus ditulis manusia, tetapi
    • gabungan AI dan Lean secara dramatis meningkatkan kecepatan penulisan dan revisi bukti
  • Sebelumnya, butuh banyak waktu untuk membuat satu makalah enak dibaca, dan
    • revisi berdasarkan masukan reviewer pun sering hanya berupa perubahan lokal
  • Namun kini, gabungan kemampuan AI untuk menghasilkan dan merevisi teks serta fungsi verifikasi dari alat bukti formal memungkinkan
    • pembuatan cepat versi baru makalah dengan berbagai tingkat presisi dan gaya penjabaran
  • Selain satu “makalah resmi”, dapat pula ada banyak versi pendamping yang dihasilkan AI
    • yang berpotensi menawarkan beragam sudut pandang dan nilai tambah tambahan

Respons Komunitas

  • Sebagian pengguna menjelaskan nilai tambah dokumen buatan AI sebagai “kemampuan melihat dari sudut yang berbeda”
  • Matematikawan lain mengangkat perlunya mengukur orisinalitas hasil AI atau kemiripannya dengan literatur yang sudah ada
    • Misalnya, ada usulan pengukuran kemiripan kuantitatif melalui perbandingan panjang bukti formal Lean
  • Komentar lain menyebut AI dapat menulis ulang makalah secara global seperti refactoring kode, sehingga
    • peneliti perlu lebih fokus pada perancangan struktur dokumen tingkat tinggi
  • Sebagian masih skeptis terhadap kemungkinan AI menggantikan peran matematikawan, tetapi
    • yang lain menilainya sebagai peluang baru untuk kolaborasi dan perluasan cara berpikir

Bacaan terkait

1 komentar

 
GN⁺ 2026-01-10
Komentar Hacker News

  • Saya bekerja di Harmonic, dan ingin meluruskan beberapa kesalahpahaman tentang Aristotle yang kami buat
    Aristotle secara aktif memanfaatkan teknik AI mutakhir, termasuk pemodelan bahasa
    Jika Anda memasukkan pembuktian informal dalam bahasa Inggris, bila pembuktian itu benar maka kemungkinan besar sistem dapat menerjemahkannya ke Lean. Dengan kata lain, ini menjadi sinyal kuat bahwa pembuktian berbahasa Inggris tersebut kokoh
    Setelah diformalkan ke Lean, tidak ada lagi keraguan bahwa pembuktian itu benar. Inilah pendekatan inti kami — jika jawaban ditemukan lewat pencarian berbasis AI, maka ketepatan hasilnya dapat dijamin terlepas dari kompleksitasnya

    • Saya penasaran bagaimana mereka memverifikasi bahwa pembuktian yang diterjemahkan AI ke Lean benar-benar merupakan formalisasi yang tepat dari masalahnya. Di bidang lain, AI generatif cukup pandai menghasilkan kebohongan yang terdengar meyakinkan, jadi saya ingin tahu apakah hal itu juga mungkin terjadi di sini
    • Saya penasaran apakah ada upaya untuk menerapkan teknologi seperti ini ke verifikasi perangkat lunak
      Rust menggunakan seperangkat aturan tetap untuk menjamin keamanan memori, tetapi aturan ini sederhana dan terbatas. Akan sangat keren jika sistem seperti Aristotle bisa diintegrasikan ke compiler, sehingga bila bukti ketepatan kode memungkinkan, kode itu bisa lolos secara otomatis
    • Setiap kali ada LLM baru, saya bingung apakah ini benar-benar kemajuan atau sekadar benchmark hacking, tetapi saya rasa formalisasi pembuktian matematika adalah indikator yang menunjukkan kemajuan nyata
      Saya penasaran berapa lama lagi sampai Harmonic bisa memformalkan sebagian besar matematika yang ditulis manusia. Pesaingnya, Christian Szegedy, katanya memperkirakan itu bisa terjadi tahun ini
    • Anda mengatakan bahwa jika pembuktian bahasa Inggrisnya benar maka kemungkinan besar bisa diterjemahkan ke Lean; saya penasaran apakah ini berbeda tergantung tingkat kesulitan per bidang dalam matematika. Setahu saya, masih banyak bidang penelitian yang bahkan sulit diformalkan oleh manusia
    • Premis “jika pernyataannya diformalkan dengan benar” terdengar seperti asumsi yang cukup besar. Seperti yang terlihat dalam kasus Navier-Stokes baru-baru ini, formalisasi itu sendiri tidak mudah

  • Dari penjelasan Terence Tao, tampaknya manusia saling memindahkan hasil antara dua alat AI, dan AI berperan mengisi celah yang ditemukan manusia
    Ini lebih dekat ke kolaborasi manusia dan AI daripada penyelesaian yang sepenuhnya otonom. Artinya, pakar memimpin dan AI membantu

    • Betul, pemahaman saya juga begitu: ini berjalan melalui interaksi antara Aristotle, ChatGPT, dan pengguna yang sangat andal
    • Saya dengar bukan Tao atau komunitasnya yang langsung menemukan celahnya, melainkan mereka menggunakan pemeriksa bukti otomatis. Justru terlihat lebih seperti rasio AI 90% / manusia 10%
    • Ada penjelasan rinci dari penulisnya di Reddit — postingan Reddit
    • Untuk memahami tingkat keahlian dan usaha manusia yang terlibat, saya sarankan membaca thread di forum masalah Erdős
    • Sebagai catatan, situs ini dibuat oleh matematikawan Thomas Bloom, dan ChatGPT membantu pengaturan teknisnya (kutipan dari FAQ)

  • Merekonstruksi pembuktian yang ada atau menggabungkannya dengan cara baru adalah proses yang membosankan atau rumit bagi manusia, tetapi AI bisa melakukannya dengan kecepatan supermanusia
    Pendekatan seperti ini akan membuka kemungkinan besar bahkan sebelum AGI tercapai. Sepertinya akan datang masa ketika matematikawan memakai AI sebagai alat untuk menangani persoalan sulit seperti Millennium Prize Problems

    • Saya rasa tidak ada batas yang jelas antara merekonstruksi pembuktian yang ada dan menciptakan matematika yang sepenuhnya baru
    • Karena matematika bersifat logis, pasti sudah ada banyak algoritma untuk eksplorasi seperti ini, jadi rasanya ini bukan sekadar masalah pencarian sederhana
    • Saya juga setuju pada bagian rekonstruksi pembuktian yang ada. Memverifikasi hasil yang dikeluarkan LLM masih merupakan pekerjaan yang membosankan, tetapi tetap lebih baik daripada melakukannya sendiri
      Nilai nyata LLM ada pada kemampuannya menawarkan sudut pandang baru pada topik yang dapat diekspresikan dalam bahasa
    • Saya menyebut fenomena ini sebagai “refactoring ilmiah”. Misalnya, AI bisa secara otomatis melakukan eksperimen seperti mengganti suatu konstanta lalu menurunkan kembali logikanya
    • Jika AI yang bisa membuktikan teorema kompleks belum bisa disebut AGI, lalu sebenarnya apa itu AGI?

  • Melihat tulisan penjelasan dari orang yang benar-benar menyelesaikan masalahnya, yang paling mengesankan adalah hasil itu didapat tanpa pipeline raksasa, hanya dengan beberapa prompt
    Model-model terbaru menggunakan sumber daya komputasi yang jauh lebih besar, jadi ini justru terlihat sebagai hasil pada batas bawah

  • Terence Tao membuat halaman wiki berjudul “AI contributions to Erdős problems”
    Melihat halaman GitHub dan postingan Mathstodon, hasil kali ini (masalah 728) adalah item hijau pertama di halaman itu, yaitu kasus pertama yang benar-benar diselesaikan AI

    • Menariknya, sebagian besar pembuktian formalisasi AI di bagian 6 wiki itu diselesaikan dalam beberapa bulan terakhir. Masa depan terlihat menjanjikan

  • Saya penasaran apakah para ahli di bidang rumit seperti fisika atau matematika juga berdialog dengan AI dan mendapatkan bantuan

    • Saya bekerja sebagai data scientist setelah postdoc di matematika murni. AI sangat membantu untuk tinjauan literatur atau saat ingin meninjau cepat matematika yang tidak saya kuasai
      Jika dilihat per bidang, kegunaannya menurun dalam urutan pemrograman > ML terapan > statistik/matematika terapan > matematika murni
    • Saya bukan berlatar fisika, tetapi berkat AI waktu yang dibutuhkan untuk mencari rumus atau makalah yang saya perlukan berkurang drastis. Namun, hasilnya tetap harus selalu diverifikasi
    • Dari sudut pandang peneliti model deep learning dan struktur attention baru, ChatGPT sangat berguna untuk pencarian makalah dan eksplorasi ide terkait
    • Sebagai penghobi matematika, LLM memberi umpan balik atas percobaan saya atau mengarahkan saya ke solusi yang sudah ada. Untuk matematika sebagai permainan, ini alat yang cukup menyenangkan
    • Saya meneliti geometri aljabar, dan selain pencarian literatur, sejauh ini belum banyak terbantu. Variasinya juga besar antar model

  • Anda bisa langsung mencoba Aristotle sekarang — https://aristotle.harmonic.fun/

    • Saya juga penasaran apakah AI diuji dengan dataset formal-conjectures dari DeepMind
    • Di dokumentasi tertulis “uvx aristotlelib@latest aristotle”, tetapi yang benar sebenarnya “uvx --from aristotlelib@latest aristotle”
      Selain itu, tautan ke halaman pribadi Stanford salah (perlu menghapus www)
    • Ini cukup menarik sampai layak dibahas dalam thread HN terpisah. Jika saya CEO-nya, saya mungkin akan menulis postingan perkenalan sendiri (tautan referensi)

  • Hasil kali ini adalah teorema tentang bilangan bulat, sebuah area yang infrastrukturnya sangat didukung oleh Mathlib
    Definisi yang digunakan juga tidak rumit, jadi jenis pembuktian seperti ini memang memiliki peluang sukses yang tinggi. Meski begitu, ini tetap pencapaian yang sangat mengejutkan

  • Ini menunjukkan potensi pendekatan AI terspesialisasi yang melampaui sekadar LLM
    Makalah Aristotle ada di arXiv:2510.01346
    Hanya karena memakai arsitektur Transformer bukan berarti semuanya LLM — jika tidak dilatih dengan data bahasa, itu tidak bisa disebut LLM

    • Sepertinya kebingungan muncul karena banyak orang memakai “LLM” dan “GenAI” secara bergantian
    • Anda bilang ini “pendekatan non-LLM”, tetapi bukankah sebenarnya ChatGPT juga digunakan?
    • Betul, pada praktiknya ChatGPT memang digunakan
    • Jika melihat makalahnya, ketiga tahapnya sama-sama melibatkan LLM besar berbasis Transformer
      1. Menangani fungsi kebijakan/nilai dalam Monte Carlo Graph Search
      2. Sistem penalaran informal menggunakan chain of thought
      3. AlphaGeometry juga memakai model bahasa neuro-simbolik
        Jadi, semua tahapnya berbasis LLM

  • Pada 2026, sepertinya AI akan semakin banyak menangani masalah matematika yang belum terpecahkan
    Kasus kali ini juga belum sepenuhnya otonom, tetapi setelah umpan balik manusia, AI tampaknya hampir menyelesaikannya sendiri
    Menurut saya, perdebatan bahwa “LLM hanyalah burung beo stokastik” kini sudah selesai. Ke depan, pusat diskusi yang sebenarnya adalah bagaimana membuatnya praktis

    • Pada 2026 tampaknya akan ada kemajuan eksplosif di bidang matematika
    • Hasil kali ini kemungkinan besar adalah remix dari pembuktian serupa yang ada di data latih, tetapi kemampuan meremix itu sendiri sangat kuat
    • Verifikasi independen tetap diperlukan. Sulit sepenuhnya mempercayai klaim perusahaan saja