Kemajuan kolaborasi manusia, AI, dan asisten pembuktian pada masalah ‘Claude Cycles’ milik Knuth
(twitter.com/BoWang87)- Bagian yang belum terselesaikan dari masalah dekomposisi Hamiltonian yang diajukan oleh Donald Knuth berhasil diperluas penyelesaiannya melalui kolaborasi manusia dan AI
- Claude menemukan solusi untuk m ganjil dan diberi nama “Claude’s Cycles”, lalu 996 dari 11.502 siklus digeneralisasi untuk semua m ganjil
- Dr. Ho Boon Suan menggunakan GPT-5.4 Pro untuk menyusun pembuktian 14 halaman untuk m genap ≥8 serta verifikasi komputasional hingga m=2000
- Dr. Keston Aquino-Michaels menemukan metode konstruksi sederhana untuk m ganjil maupun genap melalui workflow multi-agen GPT dan Claude
- Dr. Kim Morrison memverifikasi secara formal solusi Knuth dengan asisten pembuktian Lean, sehingga melengkapi ekosistem kolaborasi manusia, AI, dan alat pembuktian
Perluasan kolaborasi dalam penyelesaian masalah Claude’s Cycles
- Bagian yang belum terselesaikan dari masalah dekomposisi Hamiltonian yang diajukan oleh Donald Knuth diselesaikan melalui kolaborasi manusia dan AI
- Pada tahap awal, Claude menemukan solusi untuk m ganjil setelah sekitar satu jam eksplorasi, dan Knuth menamainya “Claude’s Cycles”
- Dalam makalah yang diperbarui, untuk kasus dasar m=3 terdapat tepat 11.502 siklus Hamiltonian, dan 996 di antaranya dapat digeneralisasi ke semua m ganjil
- Knuth mengonfirmasi 760 dekomposisi “tipe Claude” yang valid di antaranya
- Untuk m genap, Claude tidak berhasil menuntaskannya, tetapi Dr. Ho Boon Suan menggunakan GPT-5.4 Pro untuk menulis pembuktian sepanjang 14 halaman bagi m≥8 dan melakukan verifikasi komputasional hingga m=2000
- Setelah itu, Dr. Keston Aquino-Michaels menemukan metode konstruksi sederhana yang berlaku untuk m ganjil dan genap melalui workflow multi-agen yang menggunakan GPT dan Claude bersama-sama
- Dr. Kim Morrison memformalkan dan memverifikasi solusi ganjil milik Knuth di asisten pembuktian Lean
- Hasilnya, terbentuk ekosistem kolaborasi matematis yang lengkap di mana manusia, berbagai sistem AI, dan alat pembuktian formal bekerja secara paralel
- Rangkaian proses ini menunjukkan model baru riset matematika yang berkembang dari pemecahan satu masalah oleh satu AI menjadi kolaborasi multi-AI, manusia, dan asisten pembuktian
- Makalah terbaru dipublikasikan di situs Stanford CS Faculty (www-cs-faculty.stanford.edu/~knuth/papers/)
1 komentar
Opini Hacker News
Saya selalu mengatakan bahwa AI akan meraih Fields Medal sebelum bisa mengelola McDonald’s
Matematika terasa sulit bagi manusia seperti memutar sekrup dengan palu
LLM kuat dalam eksplorasi yang dangkal tetapi luas, sehingga menemukan banyak pola matematika baru
Saya memperkirakan ke depan akan ada peralihan dari LLM ke reinforcement learning ala AlphaGo berbasis pohon sintaks Lean
Jika ‘10 trik’ yang dipakai matematikawan bisa dikodekan sebagai vektor laten, maka permainan selesai
Kita berpikir dengan menerapkan geometri aljabar ke masalah teori bilangan melalui analogi geometris
AI yang dilatih dengan pohon Lean mungkin bisa memiliki sistem intuisi yang lebih luas daripada manusia
Seperti yang ditunjukkan StockFish di catur, pendekatan ini layak diteliti dari sudut pandang mechanistic interpretability
Mengambil dan memakai trik adalah sesuatu yang sudah cukup dikuasai LLM
Namun bagian merepresentasikan masalah dengan benar masih tetap menjadi ranah manusia, dan itu terasa wajar
Saya ingin menambahkan versi saya sendiri: pekerjaan terakhir yang akan diotomatisasi adalah QA
Gelombang teknologi kali ini membuat kita memikirkan ulang hakikat kerja pengetahuan, dan karena itu kita akan menjadi lebih tajam
Sejak dulu saya belajar pepatah 4chan “trolls trolling trolls”, saya selalu memandang interaksi internet dengan curiga
Saya sudah merasa Reddit menjadi ‘internet mati’, dan setelah melihat thread ini, sekarang saya bahkan tidak bisa membedakan mana bot dan mana manusia
Karena itu saya membuat layanan bernama RememberBuddy — ruang untuk menyimpan wawasan sehari-hari agar tidak terlupakan
Evolusi AI untuk matematika tampaknya akan mengikuti lintasan yang sudah diperkirakan Greg Egan dalam novel-novelnya di era 90-an
Hakikat matematika tidak berubah, tetapi alasan ‘mengapa’ melakukannya akan berubah
Dalam 『Diaspora』 karya Egan, penemuan matematika digambarkan seperti menambang permata dari tambang garam
Sebagian orang mengejar keindahan murni dari permata itu sendiri, sementara yang lain mengejar nilai praktisnya
Tempat seperti institut riset yang didirikan Terence Tao saat ini bersinggungan dengan masa depan seperti itu
Dalam jangka pendek, riset seperti ini akan sangat meningkatkan kemampuan sistem AI menghasilkan informasi yang akurat
Sebagian orang menganggap bahwa penemuan pengetahuan hanyalah meniru perilaku masa lalu, tetapi saya tidak melihatnya seperti itu
Jika seorang ahli mengarahkan model dengan baik, sebagian besar masalah bisa diselesaikan
Model sangat bagus sebagai alat untuk menggantikan pekerjaan malas para ahli, tetapi pada masalah kompleks masih ada titik buta
Saya melihat sebagian system prompt di makalah itu,
ada aturan yang berbunyi “setelah setiap eksekusi exploreXX.py, segera perbarui plan.md”
Saya penasaran mengapa prompt seperti ini meningkatkan performa pemecahan masalah tingkat lanjut
Kita makin mendekati visi CEO OpenAI tentang “intelligence as a subscription”
Mengurangi perpindahan tab masih diremehkan
Setengah dari alat AI bukan soal masalah UX, melainkan perjuangan untuk menjamin stabilitas akses ke model
“Jika 100 monyet diberi 100 senjata dan bahan bangunan, apakah mereka akan membangun rumah, atau merampok bank?”
Jika hasil itu benar-benar muncul, saya ingin bertanya apakah itu perilaku yang disengaja
Saya melihat tweet ini