Model AI China Bantu Membuktikan Konjektur Ghys dalam Tiga Dimensi, dengan Lean Memeriksa Matematikanya

Masalah matematika tahun 1995 mencapai tonggak baru

Konjektur matematika yang diajukan pada 1995 kini telah dibuktikan untuk dimensi kompleks tiga, berkat kolaborasi antara para matematikawan dan model Intern-S2 dari Shanghai AI Laboratory. Tim Universitas Peking kemudian menerjemahkan empat teorema utama dalam makalah tersebut menjadi bukti yang diperiksa oleh Lean, sistem komputer yang dirancang untuk memverifikasi penalaran matematika.

Shanghai AI Laboratory mengumumkan pencapaian tersebut pada 15 Oktober 2026, dengan menyebut tim yang dipimpin Disheng Xu, profesor di Great Bay University dan peneliti tamu di laboratorium itu. Makalah penelitian berjudul Codimension-one holomorphic Anosov diffeomorphisms mencantumkan Jiesong Zhang dari KTH Royal Institute of Technology di Swedia sebagai satu-satunya penulis.

Hasil ini menyelesaikan kasus kodimensi satu dari konjektur matematikawan Prancis Etienne Ghys, termasuk kasus dalam dimensi kompleks tiga. Konjektur tersebut menyangkut hubungan menarik antara gerak dan bentuk: apakah ruang yang mendukung jenis gerak kacau tertentu harus memiliki struktur matematika yang sangat teratur.

Intern-S2 membantu mengembangkan gagasan dan argumen melalui interaksi berulang dengan para peneliti. Dalam pernyataan tentang penggunaan AI, Zhang menyebut bahwa ia memverifikasi sendiri seluruh matematikanya. Kolaborasi ini menggabungkan eksplorasi mesin, pertimbangan manusia, dan proses verifikasi formal yang terpisah.

Laboratorium itu menyebut pencapaian ini sebagai penggunaan pertama model AI China untuk membantu memecahkan masalah matematika dengan tingkat kesulitan seperti ini. Hasil konkretnya berupa teorema klasifikasi, disertai pracetak yang tersedia untuk umum dan kode formalisasi yang dirilis secara terbuka.

Makna bukti tentang gerak dan bentuk

Konjektur Ghys termasuk dalam dinamika kompleks, yaitu kajian tentang perubahan sistem matematika ketika koordinatnya mengikuti aturan bilangan kompleks. Bilangan kompleks memiliki dua komponen riil, sehingga dimensi kompleks tiga secara lokal setara dengan enam dimensi riil. Ranah ini lebih abstrak daripada benda biasa yang bergerak di sebuah ruangan.

Sistem Anosov memiliki kombinasi peregangan dan pemampatan yang terdefinisi secara tepat. Dalam gerak berulang, beberapa arah mengerut sementara yang lain mengembang. Titik awal yang berdekatan dapat saling menjauh dengan cepat, sehingga menghasilkan perilaku kacau meskipun aturan yang mengatur setiap langkah bersifat pasti.

Bayangkan proses berulang yang meregangkan dan melipat suatu bentuk. Sistem matematika yang dikaji di sini jauh lebih ketat: peregangan dan pemampatannya harus memenuhi syarat seragam, dan geraknya harus mempertahankan struktur yang diberikan oleh koordinat kompleks.

Ghys mengajukan bahwa sistem semacam itu pada manifold kompleks kompak seharusnya memiliki deskripsi aljabar yang baku. Manifold adalah ruang yang tampak sederhana dalam lingkungan kecil, meskipun bentuk keseluruhannya dapat rumit. Dalam konteks ini, kekompakan merupakan syarat matematika yang mencegah ruang tersebut membentang tanpa batas.

Teorema Zhang menyatakan bahwa setiap difeomorfisme Anosov holomorfik kodimensi satu pada manifold kompleks terhubung yang kompak bersifat konjugat secara biholomorfik dengan suatu automorfisme hiperbolik pada torus kompleks. Dengan kata lain, perubahan koordinat yang dapat dibalik dan mempertahankan struktur kompleks mengubah gerak tersebut menjadi transformasi aljabar baku pada ruang yang sangat teratur.

Torus kompleks dapat dibangun dengan mengidentifikasi titik-titik dalam ruang kompleks yang berbeda sebesar unsur-unsur kisi berulang. Pencapaian utamanya adalah bahwa dinamika yang rumit itu mengharuskan deskripsi geometri yang teratur ini.

Mengapa cakupan yang tepat penting

Makalah ini membahas kasus kodimensi satu. Dalam sistem ini, salah satu bagian yang mengerut atau mengembang memiliki dimensi kompleks satu. Teorema tersebut mencakup keluarga terbatas ini secara umum dan menyelesaikan konjektur untuk dimensi kompleks tiga.

Konjektur Ghys yang lebih luas membahas sistem Anosov holomorfik pada cakupan manifold kompleks yang lebih beragam dan mendeskripsikannya menggunakan model aljabar baku pada ruang yang disebut manifold infra-nil kompleks. Hasil Zhang memberikan jawaban yang sangat kaku untuk kasus yang dikaji: torus kompleks dan automorfisme hiperbolik.

Bagi matematikawan yang mengkaji kasus ini, teorema tersebut mengubah persoalan dari mencari ruang dan gerak yang belum diketahui menjadi mempelajari model baku. Perubahan koordinat menghubungkan sistem semula dengan model itu sekaligus mempertahankan geometri kompleksnya.

Xu telah bertahun-tahun meneliti masalah ini. Sebelumnya, ia mengkaji kasus dimensi tiga bersama mantan pembimbingnya, peraih Medali Fields Artur Avila. Xu dan Zhang kemudian memperoleh hasil parsial terkait yang diterbitkan dalam Journal of the European Mathematical Society. Karya baru ini melanjutkan perhatian panjang mereka terhadap persoalan matematika yang sama.

Dari tes Olimpiade ke kemitraan riset

Peran Intern-S2 menyusul hasil sebelumnya yang diraih Intern-S1 dalam Olimpiade Matematika China 2025. Komite Chinese Mathematical Society yang bertanggung jawab atas kompetisi matematika tingkat sekolah menengah mengadakan tes AI pada tahun itu, dengan mengundang tiga model China untuk menyelesaikan soal dalam batas waktu yang sama dengan peserta manusia.

Intern-S1 meraih 102 poin dengan standar penilaian yang sama, menempati peringkat pertama di antara tiga model peserta. Ambang batas medali emas adalah 78 poin, sehingga nilainya 24 poin di atas ambang itu, atau sekitar 31 persen lebih tinggi.

Xu melihat potensi penggunaan keluarga model tersebut dalam riset matematika, sementara Shanghai AI Laboratory ingin beralih dari soal kompetisi ke pertanyaan yang belum terpecahkan. Kolaborasi mereka dimulai pada awal 2026 dan mencakup pembangunan sistem perangkat lunak, yang disebut Harness, untuk mengatur pekerjaan model dan interaksinya dengan para peneliti.

Tahapan utamanya adalah:

• 1995: Etienne Ghys mengajukan konjektur tersebut.
• 2025: Intern-S1 meraih 102 poin dalam tes AI Olimpiade Matematika China.
• Awal 2026: Xu dan Shanghai AI Laboratory memulai kolaborasi pelatihan model.
• Maret 2026: Xu menjadi peneliti tamu di laboratorium tersebut.
• Agustus 2026: Versi Intern-S2 yang dikembangkan secara internal beserta sistem pendukungnya mencapai tahap yang digunakan untuk eksplorasi matematika intensif.
• 29 September: Makalah Zhang diunggah ke arXiv, lalu diperbarui pada 13 Oktober.
• 15 Oktober 2026: Pencapaian tersebut diumumkan kepada publik.

Bagaimana para matematikawan membimbing AI

Eksplorasi awal Intern-S2 terhadap masalah tersebut menghasilkan laporan penurunan sekitar 400 halaman. Xu mengajak Zhang, mantan mahasiswanya yang merupakan peneliti pascadoktoral di KTH, untuk bergabung dalam upaya itu sebagai peneliti tamu. Zhang telah mengikuti konjektur Ghys sejak masa doktoralnya.

Xu dan Zhang menelaah usulan model, mengidentifikasi peluang yang menjanjikan, dan memberikan masukan untuk mengarahkan eksplorasi berikutnya. Mesin menelusuri berbagai alur penalaran dan menghasilkan argumen; para matematikawan menentukan arah mana yang layak dikembangkan lebih lanjut dan membantu menyusun bukti akhir.

Laboratorium itu menjelaskan bahwa prosesnya mencakup tujuh tahap penalaran berkelanjutan. Selama proses tersebut, graf masalah model berkembang dari 15 menjadi 389 simpul, sementara hasil yang terkumpul mencapai sekitar seribu halaman dan mencakup puluhan pendekatan yang diusulkan.

Graf masalah adalah peta tugas-tugas matematika yang lebih kecil beserta keterkaitannya. Satu simpul dapat mewakili klaim antara, sementara simpul lain mewakili hasil yang diperlukan untuk membuktikannya. Peningkatan yang dilaporkan menunjukkan seberapa luas sistem membagi dan mengeksplorasi masalah tersebut.

Pernyataan Zhang tentang penggunaan AI menjelaskan secara langsung siapa yang bertanggung jawab atas matematika dalam karya akhir itu: versi internal Intern-S2 membantu mengembangkan gagasan dan argumen melalui beberapa putaran dialog, dan ia memeriksa sendiri matematikanya. Makalahnya juga menyampaikan terima kasih kepada Xu atas diskusi berkelanjutan.

Kontribusi perangkat lunak pendukung

Shanghai AI Laboratory memadukan model tersebut dengan perangkat lunak yang dirancang untuk mengelola rangkaian penalaran panjang dan masukan manusia berulang. Sistem ini dapat membagi pertanyaan sulit menjadi tugas-tugas yang lebih kecil, mengeksplorasi beberapa arah, dan menyajikan hasil untuk dinilai para peneliti.

Pendekatan pelatihannya menggabungkan pengetahuan ilmiah yang luas dengan materi yang ditujukan untuk riset matematika, termasuk soal sulit yang diambil dari makalah matematika dan metode untuk memeriksa solusi yang diusulkan. Laboratorium itu juga menjelaskan penggunaan pembelajaran penguatan dengan imbalan yang dapat diverifikasi, artinya penalaran yang berhasil dan dapat diperiksa bisa menjadi sinyal pelatihan.

Para peneliti kemudian menggunakan pengalaman dari sistem pendukung tersebut untuk menyempurnakan model itu sendiri. Tujuan praktisnya adalah menjaga kemajuan yang berguna selama penyelidikan panjang, termasuk melacak hasil antara dan memperbaiki kesalahan seiring berkembangnya argumen baru.

Laboratorium itu juga menyebut hasil pada IMO-Proof dan AdvancedMathBench, tolok ukur yang berfokus pada penalaran matematika. Untuk proyek Ghys, bukti paling terperinci tentang cara kerja sistem adalah rangkaian penurunan yang ekstensif, masukan pakar, makalah yang telah selesai, dan verifikasi formal sesudahnya.

Bagaimana Universitas Peking memeriksa bukti

Tim Universitas Peking yang dipimpin Bin Dong dan Ruochuan Liu menggunakan kerangka kerja SHEAF untuk memformalkan keempat teorema utama dalam makalah Zhang. Pekerjaan itu juga mencakup hasil-hasil Ghys yang menjadi landasan argumen.

Formalisasi menerjemahkan definisi, asumsi, dan penalaran matematika ke dalam bahasa yang dapat diperiksa komputer. Makalah konvensional dapat mengandalkan pembaca terlatih untuk melengkapi langkah-langkah yang sudah dikenal. Lean mengharuskan langkah-langkah tersebut dinyatakan melalui pernyataan yang tepat dan operasi logis yang diizinkan.

Anggota tim Jiedong Jiang dan Bin Wu mengatakan upaya itu memakan waktu sekitar lima hari, dengan hingga 100 agen AI bekerja secara paralel. Hasilnya sekitar 550.000 baris kode Lean. Para pakar juga memeriksa bahwa pernyataan formal tersebut sesuai dengan makna matematika dari teorema-teorema utama dalam makalah.

SHEAF mengatur tugas sebagai graf berarah yang terdiri atas definisi, proposisi, dan dependensi. Dengan demikian, sejumlah agen dapat mengerjakan bagian-bagian yang saling terhubung, sementara tim melacak pernyataan mana yang sudah memiliki bukti dan mana yang masih perlu dikerjakan.

Formalisasi itu membutuhkan lebih dari sekadar menerjemahkan argumen akhir. Sejumlah hasil pendukung dalam dinamika belum tersedia di pustaka matematika formal yang ada. Tim harus menyediakan landasan tersebut atau mencari cara dengan menggunakan hasil yang sudah tersedia, lalu menghubungkan semua bagian menjadi rangkaian yang lengkap.

Makalah tersebut tersedia sebagai pracetak di arXiv, sementara kode formalisasinya telah dirilis di GitHub. Pengumuman itu tidak menyebutkan publikasi jurnal maupun keputusan penelaahan sejawat.

Mengapa kedua tahap ini saling melengkapi

Intern-S2 dan SHEAF memiliki fungsi berbeda. Yang pertama mendukung pencarian gagasan dan argumen matematika. Yang kedua membantu menyusun bukti formal yang dapat diperiksa Lean. Para matematikawan mengarahkan eksplorasi, memeriksa matematika yang dihasilkan, dan menilai apakah pernyataan formalnya mencakup teorema yang dimaksud.

Skala pekerjaan ini memperjelas pembagian tersebut. Sekitar seribu halaman keluaran eksplorasi menjadi bahan bagi sebuah makalah penelitian; proses verifikasi kemudian menghasilkan sekitar 550.000 baris kode formal. Setiap tahap mengubah pekerjaan itu menjadi bentuk berbeda yang sesuai untuk tugas berbeda.

Bagi peneliti berikutnya, makalah publik tersebut menyajikan argumen matematika, sementara kode publiknya mencatat struktur bukti formal. Definisi dan hasil pendukung yang ditambahkan selama formalisasi juga dapat menjadi landasan bagi penelitian selanjutnya di bidang yang sama.

Langkah berikutnya adalah modul verifikasi yang dapat digunakan ulang

Shanghai AI Laboratory berencana mengemas alur kerja ini sebagai modul verifikasi matematika untuk platform penemuan ilmiah Intern Duanyan. Tujuannya agar proyek selanjutnya dapat menggunakan kembali perpaduan eksplorasi model, masukan pakar, dan pemeriksaan formal.

Laboratorium itu juga berniat menerapkan kemampuan penalaran yang dikembangkan melalui proyek ini ke disiplin lain yang memiliki struktur matematika terkait. Siklus yang diusulkan adalah menyelesaikan masalah riset, mengubah metode yang berguna menjadi perangkat lunak yang dapat digunakan ulang, lalu menerapkannya pada penyelidikan lain.

Bagi Xu, hasil ini memperluas minat riset yang telah lama ia tekuni melalui kolaborasi Great Bay University, Shanghai AI Laboratory, KTH, dan Universitas Peking. Bagi komunitas matematika yang lebih luas, hasil ini menawarkan temuan klasifikasi baru sekaligus contoh terperinci tentang keterlibatan AI dalam riset di bawah arahan manusia.

Poin-poin Utama

• Bukti baru ini menyelesaikan kasus kodimensi satu dari konjektur Ghys, termasuk dimensi kompleks tiga.
• Jiesong Zhang adalah satu-satunya penulis makalah penelitian tersebut dan menyatakan bahwa ia memverifikasi sendiri seluruh matematikanya.
• Disheng Xu dan Zhang membimbing Intern-S2 melalui eksplorasi berulang dan pemberian masukan.
• Graf masalah model berkembang dari 15 menjadi 389 simpul, dengan hasil penurunan sekitar seribu halaman.
• Kerangka kerja SHEAF dari Universitas Peking membantu memformalkan empat teorema utama dan hasil pendukung dalam Lean.
• Upaya verifikasi dilaporkan memakan waktu sekitar lima hari dan menghasilkan sekitar 550.000 baris kode.
• Laboratorium itu berencana mengubah alur kerja tersebut menjadi modul verifikasi matematika yang dapat digunakan ulang.