Model AI China Bantu Membuktikan Konjektur Ghys dalam Tiga Dimensi, dengan Lean Menyemak Matematiknya

Masalah matematik 1995 mencapai pencapaian baharu

Satu konjektur matematik yang dikemukakan pada 1995 kini dibuktikan bagi dimensi kompleks tiga, hasil kerjasama antara ahli matematik dengan model Intern-S2 dari Makmal AI Shanghai. Pasukan Universiti Peking kemudian menterjemahkan empat teorem utama dalam makalah itu menjadi bukti yang disemak oleh Lean, sebuah sistem komputer yang direka untuk mengesahkan penaakulan matematik.

Makmal AI Shanghai mengumumkan pencapaian itu pada 15 Oktober 2026, dengan memberikan penghargaan kepada pasukan yang diketuai Disheng Xu, profesor di Universiti Great Bay dan sarjana pelawat di makmal tersebut. Makalah penyelidikan, Codimension-one holomorphic Anosov diffeomorphisms, menyenaraikan Jiesong Zhang dari Institut Teknologi Diraja KTH Sweden sebagai pengarang tunggal.

Hasil itu menyelesaikan kes kodimensi satu bagi konjektur ahli matematik Perancis, Etienne Ghys, termasuk kes dalam dimensi kompleks tiga. Ia menyentuh hubungan menarik antara gerakan dengan bentuk: sama ada ruang yang menyokong jenis gerakan huru-hara tertentu semestinya mempunyai struktur matematik yang sangat teratur.

Intern-S2 membantu mengembangkan idea dan hujah melalui pertukaran berulang dengan para penyelidik. Dalam perisytiharan penggunaan AI, Zhang menyatakan bahawa beliau mengesahkan sendiri semua matematik tersebut. Kerjasama itu menggabungkan penerokaan mesin, pertimbangan manusia dan proses pengesahan formal yang berasingan.

Makmal itu menyifatkan pencapaian tersebut sebagai penggunaan pertama model AI China untuk membantu menyelesaikan masalah matematik pada tahap ini. Hasil konkritnya ialah teorem pengelasan, disertai praterbitan awam dan kod pemformalan yang turut dikeluarkan kepada umum.

Perkara yang dibuktikan tentang gerakan dan bentuk

Konjektur Ghys tergolong dalam dinamik kompleks, iaitu kajian tentang perubahan sistem matematik apabila koordinatnya mengikut peraturan nombor kompleks. Nombor kompleks mempunyai dua komponen nyata, maka dimensi kompleks tiga bersamaan dengan enam dimensi nyata secara setempat. Kerangka ini lebih abstrak daripada objek biasa yang bergerak di dalam bilik.

Sistem Anosov mempunyai gabungan pengembangan dan pengecutan yang ditakrifkan secara tepat. Apabila gerakan berulang, sesetengah arah mengecut manakala yang lain mengembang. Titik permulaan yang berdekatan boleh berpisah dengan cepat, lalu menghasilkan tingkah laku huru-hara walaupun peraturan yang mengawal setiap langkah adalah tepat.

Satu gambaran mudah ialah proses berulang yang meregangkan dan melipat sesuatu bentuk. Sistem matematik yang dikaji di sini jauh lebih terhad: regangan dan pengecutannya mesti memenuhi syarat seragam, dan gerakannya mesti mengekalkan struktur yang ditentukan oleh koordinat kompleks.

Ghys mengemukakan bahawa sistem sedemikian pada manifold kompleks kompak sepatutnya mempunyai penerangan algebra piawai. Manifold ialah ruang yang kelihatan ringkas dalam kejiranan kecil, walaupun bentuk keseluruhannya mungkin rumit. Kekompakan ialah syarat matematik yang, dalam konteks ini, menghalang ruang daripada berlanjutan tanpa batas.

Teorem Zhang menyatakan bahawa setiap difeomorfisme Anosov holomorfik kodimensi satu pada manifold kompleks bersambung yang kompak adalah konjugat biholomorfik kepada automorfisme hiperbolik bagi suatu torus kompleks. Ringkasnya, perubahan koordinat boleh balik yang menghormati struktur kompleks menukarkan gerakan itu kepada transformasi algebra piawai pada ruang yang sangat teratur.

Torus kompleks boleh dibina dengan mengenal pasti titik-titik dalam ruang kompleks yang berbeza mengikut unsur daripada kekisi berulang. Pencapaian utamanya ialah dinamik yang rumit itu memaksa gambaran geometri yang teratur ini.

Mengapa skop yang tepat itu penting

Makalah itu meneliti kes kodimensi satu. Bagi sistem ini, ertinya salah satu bahagian yang mengecut atau mengembang mempunyai dimensi kompleks satu. Teorem itu meliputi keluarga terhad ini secara umum dan menyelesaikan konjektur tersebut dalam dimensi kompleks tiga.

Konjektur Ghys yang lebih luas merangkumi sistem Anosov holomorfik pada julat manifold kompleks yang lebih besar dan menghuraikannya menggunakan model algebra piawai pada ruang yang dipanggil manifold infra-nil kompleks. Hasil Zhang memberikan jawapan yang sangat tegar bagi kes yang dikaji: torus kompleks dan automorfisme hiperbolik.

Bagi ahli matematik yang mengkaji kes ini, teorem tersebut mengalihkan masalah daripada mengenal pasti ruang dan gerakan yang belum diketahui kepada kajian model piawai. Perubahan koordinat menghubungkan sistem asal dengan model itu sambil mengekalkan geometri kompleksnya.

Xu telah mengkaji masalah itu selama bertahun-tahun. Sebelum ini, beliau menyiasat kes dimensi tiga bersama bekas penasihatnya, penerima Pingat Fields, Artur Avila. Xu dan Zhang kemudian memperoleh hasil separa berkaitan yang diterbitkan dalam Journal of the European Mathematical Society. Karya baharu ini dibina berasaskan penelitian berterusan terhadap persoalan matematik yang sama.

Daripada ujian Olimpik kepada kerjasama penyelidikan

Peranan Intern-S2 menyusuli pencapaian terdahulu Intern-S1 dalam Olimpik Matematik China 2025. Jawatankuasa Persatuan Matematik China yang bertanggungjawab terhadap pertandingan matematik sekolah menengah memperkenalkan ujian AI pada tahun itu, dengan menjemput tiga model China menyelesaikan masalah dalam tempoh masa yang sama seperti peserta manusia.

Intern-S1 memperoleh 102 mata mengikut piawaian pemarkahan yang sama, menduduki tempat pertama dalam kalangan tiga model yang mengambil bahagian. Ambang pingat emas ialah 78 mata, menjadikan skornya 24 mata lebih tinggi daripada ambang itu, atau kira-kira 31 peratus lebih tinggi.

Xu melihat potensi penggunaan keluarga model itu dalam penyelidikan matematik, manakala Makmal AI Shanghai mahu beralih daripada masalah pertandingan kepada persoalan yang belum terjawab. Kerjasama mereka bermula pada awal 2026 dan merangkumi pembinaan sistem perisian, yang digambarkan sebagai Harness, untuk menyusun kerja model itu serta pertukarannya dengan para penyelidik.

Peringkat utamanya ialah:

• 1995: Etienne Ghys mengemukakan konjektur tersebut.
• 2025: Intern-S1 memperoleh 102 mata dalam ujian AI Olimpik Matematik China.
• Awal 2026: Xu dan Makmal AI Shanghai memulakan kerjasama latihan model.
• Mac 2026: Xu menjadi sarjana pelawat di makmal tersebut.
• Ogos 2026: Versi Intern-S2 yang dibangunkan secara dalaman bersama sistem sokongannya mencapai tahap yang digunakan untuk penerokaan matematik intensif.
• 29 September: Makalah Zhang dimuat naik ke arXiv, diikuti semakan pada 13 Oktober.
• 15 Oktober 2026: Pencapaian itu diumumkan kepada umum.

Bagaimana ahli matematik membimbing AI

Penerokaan awal Intern-S2 terhadap masalah itu menghasilkan laporan penerbitan terbitan sepanjang kira-kira 400 halaman. Xu menjemput Zhang, bekas pelajarnya dan penyelidik pascadoktoral di KTH, untuk menyertai usaha itu sebagai sarjana pelawat. Zhang telah mengikuti konjektur Ghys sejak pengajian doktoralnya.

Xu dan Zhang meneliti cadangan model itu, mengenal pasti pembukaan yang menjanjikan dan memberikan maklum balas untuk membimbing penerokaan seterusnya. Mesin itu menelusuri cabang-cabang penaakulan dan menghasilkan hujah; ahli matematik menentukan arah yang wajar diteruskan serta membantu menyusun bukti akhir.

Makmal itu melaporkan tujuh kelompok penaakulan lanjutan. Sepanjang proses tersebut, graf masalah model itu berkembang daripada 15 nod kepada 389, manakala jumlah hasil terkumpul mencecah kira-kira seribu halaman dan merangkumi puluhan pendekatan yang dicadangkan.

Graf masalah ialah peta tugas matematik yang lebih kecil serta hubung kaitnya. Satu nod mungkin mewakili dakwaan perantaraan, manakala nod lain mewakili hasil yang diperlukan untuk membuktikannya. Pertambahan yang dilaporkan itu menunjukkan sejauh mana sistem tersebut membahagikan dan meneroka masalah berkenaan.

Perisytiharan penggunaan AI oleh Zhang menerangkan secara langsung tanggungjawab terhadap matematik yang dimuktamadkan: versi dalaman Intern-S2 membantu mengembangkan idea dan hujah melalui beberapa pusingan dialog, dan beliau menyemak sendiri matematik tersebut. Makalahnya turut merakamkan penghargaan kepada Xu atas perbincangan berterusan.

Sumbangan perisian sokongan

Makmal AI Shanghai menggandingkan model itu dengan perisian yang direka untuk mengurus rantaian penaakulan yang panjang serta maklum balas manusia yang berulang. Sistem itu boleh memecahkan soalan sukar kepada tugas yang lebih kecil, meneroka beberapa arah dan mengembalikan hasil untuk dinilai oleh para penyelidik.

Pendekatan latihan itu menggabungkan pengetahuan saintifik yang luas dengan bahan yang menyasarkan matematik penyelidikan, termasuk masalah sukar daripada makalah matematik dan kaedah untuk menyemak penyelesaian yang dicadangkan. Makmal itu turut menerangkan penggunaan pembelajaran pengukuhan dengan ganjaran yang boleh disahkan, iaitu penaakulan yang berjaya dan boleh disemak dapat memberikan isyarat latihan.

Para penyelidik kemudian menggunakan pengalaman daripada sistem sokongan itu untuk menambah baik model berkenaan. Matlamat praktikalnya adalah untuk mengekalkan kemajuan yang berguna sepanjang penyiasatan yang panjang, termasuk menjejak hasil perantaraan dan membetulkan kesilapan apabila hujah baharu dibangunkan.

Makmal itu turut memetik hasil pada IMO-Proof dan AdvancedMathBench, penilaian yang memfokuskan penaakulan matematik. Bagi projek Ghys, bukti paling terperinci tentang cara sistem itu beroperasi ialah rangkaian penerbitan terbitan yang meluas, maklum balas pakar, makalah yang lengkap dan pengesahan formal selepasnya.

Bagaimana Universiti Peking menyemak bukti

Pasukan Universiti Peking yang diketuai Bin Dong dan Ruochuan Liu menggunakan kerangka SHEAF untuk memformalkan keempat-empat teorem utama dalam makalah Zhang. Usaha itu turut merangkumi hasil oleh Ghys yang menjadi sandaran hujah-hujah tersebut.

Pemformalan menterjemahkan takrifan, andaian dan penaakulan matematik ke dalam bahasa yang boleh disemak oleh komputer. Makalah konvensional boleh bergantung pada pembaca terlatih untuk melengkapkan langkah-langkah yang lazim. Lean menghendaki langkah-langkah itu dinyatakan melalui pernyataan yang tepat dan operasi logik yang dibenarkan.

Anggota pasukan Jiedong Jiang dan Bin Wu berkata usaha itu mengambil masa kira-kira lima hari, dengan sehingga 100 ejen AI beroperasi secara selari. Usaha tersebut menghasilkan kira-kira 550,000 baris kod Lean. Pakar turut menyemak bahawa pernyataan formal itu menepati maksud matematik teorem utama dalam makalah tersebut.

SHEAF menyusun tugas itu sebagai graf berarah yang menghubungkan takrifan, proposisi dan kebergantungan. Ini membolehkan ejen berbeza mengerjakan bahagian yang saling berkaitan, sementara pasukan menjejak pernyataan yang sudah mempunyai bukti dan yang masih memerlukan kerja.

Pemformalan itu memerlukan lebih daripada sekadar menterjemahkan hujah akhir. Beberapa hasil sokongan dalam dinamik belum tersedia dalam pustaka matematik formal sedia ada. Pasukan itu perlu menyediakan asas tersebut atau mencari laluan menggunakan hasil yang sudah tersedia, kemudian menghubungkan semua bahagian menjadi rangkaian lengkap.

Makalah itu tersedia sebagai praterbitan arXiv, manakala kod pemformalan telah dikeluarkan di GitHub. Pengumuman itu tidak menyatakan sebarang penerbitan jurnal atau keputusan semakan rakan sebaya.

Mengapa kedua-dua peringkat ini saling melengkapi

Intern-S2 dan SHEAF mempunyai tujuan berbeza. Yang pertama menyokong pencarian idea dan hujah matematik. Yang kedua membantu membina bukti formal yang boleh disemak oleh Lean. Ahli matematik membimbing penerokaan, menyemak matematik yang terhasil dan menilai sama ada pernyataan formal itu merangkumi teorem yang dimaksudkan.

Skala usaha itu menjadikan pembahagian tersebut jelas. Kira-kira seribu halaman hasil penerokaan menjadi asas kepada makalah penyelidikan; proses pengesahan pula menghasilkan kira-kira 550,000 baris kod formal. Setiap peringkat menukarkan hasil kerja itu kepada bentuk berbeza yang sesuai untuk tugas masing-masing.

Bagi penyelidik akan datang, makalah awam itu membentangkan hujah matematik, manakala kod awam merekodkan struktur bukti formal. Takrifan dan hasil sokongan yang ditambah semasa pemformalan juga mungkin menjadi titik permulaan bagi penyelidikan seterusnya dalam bidang yang sama.

Langkah seterusnya ialah modul pengesahan yang boleh digunakan semula

Makmal AI Shanghai merancang untuk membungkus aliran kerja itu sebagai modul pengesahan matematik bagi platform penemuan saintifik Intern Duanyan. Tujuannya adalah membolehkan projek seterusnya menggunakan semula gabungan penerokaan model, maklum balas pakar dan semakan formal.

Makmal itu juga berhasrat menerapkan keupayaan penaakulan yang dibangunkan melalui projek ini kepada disiplin lain yang mempunyai struktur matematik berkaitan. Kitaran yang dicadangkan adalah menyelesaikan masalah penyelidikan, menjadikan kaedah yang berguna sebagai perisian yang boleh digunakan semula dan menerapkannya pada penyiasatan lain.

Bagi Xu, hasil itu mengembangkan minat penyelidikannya yang telah lama diceburi melalui kerjasama antara Universiti Great Bay, Makmal AI Shanghai, KTH dan Universiti Peking. Bagi komuniti matematik yang lebih luas, hasil ini menawarkan teorem pengelasan baharu serta contoh terperinci tentang penglibatan AI dalam penyelidikan di bawah bimbingan manusia.

Perkara Utama

• Bukti baharu itu menyelesaikan kes kodimensi satu bagi konjektur Ghys, termasuk dimensi kompleks tiga.
• Jiesong Zhang ialah pengarang tunggal makalah penyelidikan itu dan menyatakan bahawa beliau mengesahkan sendiri semua matematik tersebut.
• Disheng Xu dan Zhang membimbing Intern-S2 melalui penerokaan serta maklum balas berulang.
• Graf masalah model itu berkembang daripada 15 nod kepada 389, dengan kira-kira seribu halaman penerbitan terbitan.
• Kerangka SHEAF Universiti Peking membantu memformalkan empat teorem utama dan hasil sokongan dalam Lean.
• Usaha pengesahan itu dilaporkan mengambil masa kira-kira lima hari dan menghasilkan kira-kira 550,000 baris kod.
• Makmal itu merancang menjadikan aliran kerja tersebut modul pengesahan matematik yang boleh digunakan semula.