Sebuah tim peneliti di Starfleet Math baru saja mengungkapkan pencapaian yang mengguncang dunia matematika: mereka berhasil memecahkan 20 masalah terbuka yang dikumpulkan oleh legendaris Paul Erdős, dengan bantuan 20 instance Codex dari OpenAI yang dijalankan secara bersamaan. Hasilnya tidak hanya berupa jawaban numerik, melainkan bukti formal lengkap yang diverifikasi oleh pembuktian teorema Lean, standar emas keabsahan matematika modern. Pencapaian ini menandai titik balik di mana kecerdasan buatan tidak lagi sekadar alat bantu, tapi aktiver dalam penemuan bukti yang selama puluhan tahun menentang para ahli.
Di antara 20 masalah itu, Soal Erdős #123 menarik perhatian khusus. Soal ini menanyakan apakah setiap bilangan bulat cukup besar dapat ditulis sebagai jumlah bilangan berbentuk a^k b^l c^m — dengan a, b, c saling prima relatif dan lebih besar dari 1 — dengan syarat ketat: tidak ada suku yang membagi suku lain. Hadiahnya $250, tapi nilai ilmiahnya jauh melampaui nominal uang. Tim membuktikan jawabannya: ya, untuk setiap triple a, b, c yang memenuhi syarat, setiap bilangan cukup besar memang bisa direpresentasikan seperti itu. Bukti formalnya kini tersimpan di Lean sebagai teorema `Erdos123.erdos_123`.
Latar belakang masalah ini klasik namun jahat. Erdős mengajukan puluhan masalah teori bilangan sejak abad ke-20, banyak yang menawarkan hadiah uang dari kantong pribadinya. Beberapa terselesaikan, tapi banyak yang bertahan hingga era digital. Pendekatan tradisional mengandalkan induksi dan sistem residu lengkap, tapi selalu gagal pada tahap "benih" — interval awal yang harus cukup lebar secara multiplikatif agar induksi bisa berlanjut. Lebar aditif saja tidak cukup; batas bawah interval harus terkendali kuantitatif. Inilah mengapa ide-ide menarik seperti identitas bertanda atau argumen Van der Waerden tidak pernah menyentuh garis finish.
Kunci terobosan tim Starfleet Math terletak pada dua langkah struktural. Pertama, mereka memindahkan seluruh konstruksi ke satu tingkat eksponen homogen: i + j + k = D. Di tingkat ini, tidak ada dua monomial yang saling membagi — sifat primitif jadi gratis. Kedua, mereka membangun "kode tepi" yang menghasilkan c^n jumlah subset primitif dengan residu berbeda modulo c^n dan carry terbatas. Melewati pewarnaan carry dan menerapkan teorema Van der Waerden terbatas (yang sudah ada di Mathlib via Hales–Jewett), mereka memperoleh deret aritmetika panjang tak terbatas dari jumlah subset homogen tersebut.
Langkah selanjutnya mengubah satu deret aritmetika menjadi interval kisi yang masif. Dengan mengurutkan basis 1 < a < c < b, mereka mendefinisikan bobot translasi A = a^{u+v} dan B = b^u c^v, lalu menyalin keluarga digit deret aritmetika menggunakan kombinasi linear A^{M-r} B^r. Lema radiks homogen terbatas membuktikan jumlah koefisien dengan batas 0 ≤ s_r < 4AB mengandung interval penuh lebar minimal 2AB^{M+1}. Mengganti setiap koefisien dengan himpunan digit deret aritmetika mewujudkan interval pada kisi langkah abc·d.
Koreksi residu kemudian mengisi celah untuk mengubah interval kisi jadi interval bilangan bulat berurutan. Koreksi ini dibangun di tiga bidang koordinat, ukurannya dibatasi C_corr c^D, dan karena B / c^{u+v} = (b/c)^u > 1, dominasi eksponensial menjamin sebaran koreksi akhirnya jauh lebih kecil dari lebar radiks. Hasil akhir: interval berurutan [L_M, U_M] dengan lebar minimal abc·B^M dan batas bawah L_M ≤ K·B^{M+1} — persis benih yang dibutuhkan induksi untuk meloncat ke tak hingga.
Seluruh rantai bukti ini dikodekan ke Lean 4, memanfaatkan pustaka Mathlib yang sudah kaya. Proses formalisasi memaksa peneliti membuat setiap langkah eksplisit, menemukan celah halus yang terlewat di bukti kertas. Hasilnya bukan sekadar keyakinan, tapi sertifikat matematis yang bisa dicek mesin oleh siapa saja. Ini model baru: AI menghasilkan kandidat bukti, manusia mengarahkan strategi tingkat tinggi, dan pembuktian teorema mengunci keabsahan.
Bagi komunitas matematika Indonesia, pencapaian ini membawa pesan ganda. Pertama, formalisasi Lean bukan lagi domain eksklusif universitas elit Barat; Mathlib bersifat terbuka dan bisa diakses dari mana saja. Kedua, alat AI seperti Codex menurunkan hambatan masuk: mahasiswa ITB, UI, atau UGM yang punya latar belakang teori bilangan dan pemrograman fungsional kini bisa ikut berkontribusi ke depan pengetahuan global tanpa perlu grant besar. Komunitas Lean Indonesia yang tumbuh lewat grup Discord dan GitHub lokal sudah mulai menerjemahkan dokumentasi dan mengorganisir *lean-do* bulanan.
Di sisi industri, startup AI lokal yang fokus pada *code generation* dan *formal verification* — seperti yang berkembang di ekosistem Jakarta dan Bandung — mendapat validasi pasar: teknologi ini bukan hype, tapi alat produksi nyata untuk penemuan ilmiah. Kementerian Pendidikan, Kebudayaan, Riset, dan Teknologi (Kemendikbudristek) yang sedang mendorong *open science* dan *digital transformation* bisa mempertimbangkan insentif bagi tim yang memformalkan hasil penelitian dasar ke Lean, mempercepat adopsi standar bukti terverifikasi di jurnal nasional.
Masa depan penelitian matematika kemungkinan besar akan berbentuk *human–AI–prover* triad. Erdős sendiri, yang terkenal kolaboratif dan suka menawarkan hadiah untuk soal yang ia rasa menarik, mungkin akan tersenyum melihat 20 akun AI berlari paralel mengejar jejak pemikirannya. Bagi generasi muda Indonesia, pintu itu terbuka: pelajari Lean, eksperimen dengan Codex atau model terbuka sejenis, dan siapa tahu nama Anda yang berikutnya terukir di daftar pemecah masalah Erdős — kini dengan bantuan silikon, tapi tetap bermartabat manusia.