Tumulong ang Modelong AI ng Tsina na Patunayan ang Hula ni Ghys sa Tatlong Dimensiyon; Sinuri ng Lean ang Matematika

Naabot ng isang problemang matematikal mula 1995 ang bagong mahalagang yugto

Nagbunga ng patunay para sa complex dimension three ang isang matematikal na haka-haka na iminungkahi noong 1995, kasunod ng pagtutulungan ng mga matematikong at ng modelong Intern-S2 ng Shanghai AI Laboratory. Isinalin naman ng isang pangkat mula sa Peking University ang apat na pangunahing teorema ng papel tungo sa mga patunay na sinuri ng Lean, isang sistemang pangkompyuter na idinisenyo upang beripikahin ang pangangatwirang matematikal.

Inanunsyo ng Shanghai AI Laboratory ang tagumpay noong Oktubre 15, 2026, at kinilala ang pangkat na pinamumunuan ni Disheng Xu, propesor sa Great Bay University at visiting scholar sa laboratoryo. Nakalista sa papel-pananaliksik na Codimension-one holomorphic Anosov diffeomorphisms si Jiesong Zhang ng KTH Royal Institute of Technology ng Sweden bilang nag-iisang may-akda.

Lutas ng resulta ang codimension-one case ng haka-haka ng Pranses na matematikong si Etienne Ghys, kabilang ang kaso sa complex dimension three. Tungkol ito sa kapansin-pansing ugnayan ng galaw at hugis: kung ang isang espasyong sumusuporta sa isang partikular na uri ng magulong galaw ay dapat ding magkaroon ng napakaayos na estrukturang matematikal.

Tumulong ang Intern-S2 sa pagbuo ng mga ideya at argumento sa pamamagitan ng paulit-ulit na palitan ng kuro-kuro sa mga mananaliksik. Isinaad ni Zhang sa kanyang deklarasyon tungkol sa paggamit ng AI na siya mismo ang nagsuri sa lahat ng matematika. Pinagsama ng pagtutulungan ang pagsasaliksik ng makina, paghatol ng tao at hiwalay na proseso ng pormal na beripikasyon.

Inilarawan ng laboratoryo ang tagumpay bilang unang paggamit ng modelong AI mula sa Tsina upang tumulong lumutas ng problemang matematikal na ganito kahalaga. Ang kongkretong resulta ay isang teorema ng klasipikasyon, kalakip ang paunang bersiyong inilathala sa publiko at pormalisasyong code na inilabas din sa publiko.

Ang sinasabi ng patunay tungkol sa galaw at hugis

Nabibilang sa complex dynamics ang haka-haka ni Ghys, ang pag-aaral kung paano nagbabago ang mga sistemang matematikal kapag sumusunod sa mga tuntunin ng complex numbers ang kanilang mga koordinado. May dalawang real component ang isang complex number, kaya katumbas ng anim na real dimension ang complex dimension three sa lokal na antas. Mas abstrakto ang tagpuang ito kaysa sa karaniwang bagay na gumagalaw sa isang silid.

May tiyak na kombinasyon ng pag-unat at pagsiksik ang isang Anosov system. Sa paulit-ulit na paggalaw, kumikipot ang ilang direksiyon habang lumalawak naman ang iba. Mabilis na maaaring magkalayo ang mga panimulang puntong magkakalapit, na nagbubunga ng magulong kilos kahit eksakto ang tuntuning namamahala sa bawat hakbang.

Isang kapaki-pakinabang na larawan nito ang paulit-ulit na prosesong nag-uunat at nagtitiklop ng isang hugis. Higit na mahigpit ang mga kondisyong ipinapataw sa sistemang matematikal na pinag-aaralan dito: kailangang tumupad sa pare-parehong kundisyon ang pag-unat at pag-urong nito, at kailangang mapanatili ng galaw ang estrukturang ibinibigay ng mga complex coordinate.

Iminungkahi ni Ghys na dapat magkaroon ng karaniwang deskripsiyong alhebraiko ang ganitong mga sistema sa mga compact complex manifold. Ang manifold ay isang espasyong mukhang simple sa maliit na paligid, kahit komplikado ang kabuuang hugis nito. Sa tagpuang ito, isa sa mga kahulugan ng compactness ay hindi umaabot nang walang hanggan ang espasyo.

Sinasabi ng teorema ni Zhang na ang bawat codimension-one holomorphic Anosov diffeomorphism sa isang compact connected complex manifold ay biholomorphically conjugate sa isang hyperbolic automorphism ng isang complex torus. Sa mas payak na pananalita, ginagawang karaniwang pagbabagong alhebraiko sa isang napakaayos na espasyo ang galaw sa pamamagitan ng nababaligtad na pagbabago ng mga koordinado na gumagalang sa complex structure.

Maaaring buuin ang isang complex torus sa pamamagitan ng pagtukoy na magkapareho ang mga puntong nagkakaiba sa complex space ng mga elemento ng isang paulit-ulit na lattice. Ang pangunahing tagumpay ay pinipilit ng komplikadong dynamics na magkaroon ng ganitong maayos na heometrikong paglalarawan.

Bakit mahalaga ang tiyak na saklaw

Tinutugunan ng papel ang codimension-one setting. Para sa mga sistemang ito, nangangahulugan itong may complex dimension one ang isa sa mga bahaging kumikipot o lumalawak. Sinasaklaw ng teorema ang limitadong pamilyang ito sa pangkalahatan at nilulutas ang haka-haka sa complex dimension three.

Tungkol ang mas malawak na haka-haka ni Ghys sa mga holomorphic Anosov system sa mas maraming uri ng complex manifold, at inilalarawan ang mga ito gamit ang karaniwang modelong alhebraiko sa mga espasyong tinatawag na complex infra-nilmanifold. Nagbibigay ang resulta ni Zhang ng partikular na mahigpit na sagot para sa kasong pinag-aralan: isang complex torus at isang hyperbolic automorphism.

Para sa mga matematikong nagtatrabaho sa kasong ito, inililipat ng teorema ang problema mula sa pagtukoy sa di-kilalang espasyo at galaw tungo sa pag-aaral ng karaniwang modelo. Iniuugnay ng pagbabago ng mga koordinado ang orihinal na sistema sa modelong iyon habang pinananatili ang complex geometry.

Taon nang pinag-aaralan ni Xu ang problemang ito. Dati niyang siniyasat ang kaso sa dimension three kasama ang dati niyang tagapayo na si Artur Avila, nagwagi ng Fields Medal. Nang maglaon, nakakuha sina Xu at Zhang ng mga kaugnay na bahagyang resulta na inilathala sa Journal of the European Mathematical Society. Bunga ang bagong pag-aaral ng matagal na pagtutok sa iisang tanong na matematikal.

Mula sa pagsusulit sa Olympiad tungo sa pakikipagtulungan sa pananaliksik

Kasunod ang papel ng Intern-S2 ng naunang resulta ng Intern-S1 sa Chinese Mathematical Olympiad noong 2025. Nagpakilala noong taong iyon ng pagsusulit sa AI ang komiteng nangangasiwa sa mga paligsahan sa matematika para sa sekondaryang paaralan ng Chinese Mathematical Society, at inimbitahan ang tatlong modelong Tsino na lumutas ng mga problema sa kaparehong takdang oras ng mga taong kalahok.

Umiskor ang Intern-S1 ng 102 puntos sa ilalim ng kaparehong pamantayan sa pagmamarka, kaya nanguna ito sa tatlong modelong lumahok. 78 puntos ang hangganan para sa gintong medalya, kaya 24 puntos, o humigit-kumulang 31 porsiyento, na mas mataas dito ang iskor ng modelo.

Nakita ni Xu ang potensiyal na gamitin sa matematikal na pananaliksik ang pamilya ng mga modelo, samantalang nais ng Shanghai AI Laboratory na lumipat mula sa mga problema sa paligsahan tungo sa mga tanong na wala pang kalutasan. Nagsimula ang kanilang pagtutulungan noong unang bahagi ng 2026 at kabilang dito ang pagbuo ng isang sistemang software na tinawag na Harness, upang isaayos ang gawain ng modelo at ang palitan nito ng mga mananaliksik.

Ang mga pangunahing yugto ay:

• 1995: Iminungkahi ni Etienne Ghys ang haka-haka.
• 2025: Umiskor ang Intern-S1 ng 102 puntos sa pagsusulit sa AI ng Chinese Mathematical Olympiad.
• Unang bahagi ng 2026: Sinimulan nina Xu at ng Shanghai AI Laboratory ang pagtutulungan sa pagsasanay ng modelo.
• Marso 2026: Naging visiting scholar si Xu sa laboratoryo.
• Agosto 2026: Umabot sa yugtong ginamit para sa masinsinang pagsasaliksik matematikal ang bersiyong binuo sa loob ng organisasyon ng Intern-S2 at ang pansuportang sistema nito.
• Setyembre 29: Inilathala sa arXiv ang papel ni Zhang, at sinundan ito ng rebisyon noong Oktubre 13.
• Oktubre 15, 2026: Ipinahayag sa publiko ang tagumpay.

Paano ginabayan ng mga matematikong ang AI

Sa unang pagsasaliksik ng Intern-S2 sa problema, nakabuo ito ng ulat ng derivation na humigit-kumulang 400 pahina. Inanyayahan ni Xu si Zhang, dati niyang estudyante at postdoctoral researcher sa KTH, na sumali sa gawain bilang visiting scholar. Sinusubaybayan na ni Zhang ang haka-haka ni Ghys mula pa noong doktoral niyang pag-aaral.

Sinuri nina Xu at Zhang ang mga mungkahi ng modelo, tinukoy ang mga posibleng mabungang panimulang punto at nagbigay ng puna upang gabayan ang kasunod na pagsasaliksik. Sinundan ng makina ang iba’t ibang sangay ng pangangatwiran at bumuo ng mga argumento; nagpasya naman ang mga matematikong kung aling direksiyon ang dapat pang paglaanan ng trabaho at tumulong silang buuin ang pinal na patunay.

Inilarawan ng laboratoryo ang pitong batch ng tuluy-tuloy na pangangatwiran. Habang nagpapatuloy ang proseso, lumawak ang problem graph ng modelo mula 15 node tungo sa 389, umabot sa humigit-kumulang isang libong pahina ang naipong output at kabilang dito ang dose-dosenang mungkahing paraan.

Mapa ang problem graph ng mas maliliit na gawaing matematikal at ng mga ugnayan ng mga ito. Maaaring kumatawan ang isang node sa isang pansamantalang pahayag, habang kumakatawan naman ang isa pa sa resultang kailangan upang mapatunayan ito. Ipinakikita ng iniulat na paglaki kung gaano kalawak hinati at sinaliksik ng sistema ang problema.

Direktang inilalarawan sa deklarasyon ni Zhang tungkol sa paggamit ng AI kung sino ang may pananagutan sa natapos na matematika: tumulong ang isang panloob na bersiyon ng Intern-S2 sa pagbuo ng mga ideya at argumento sa maraming round ng pag-uusap, at siya mismo ang nagsuri sa matematika. Nagpasalamat din siya sa papel kay Xu para sa tuluy-tuloy na talakayan.

Ambag ng pansuportang software

Itinambal ng Shanghai AI Laboratory ang modelo sa software na nilayong mamahala sa mahahabang hanay ng pangangatwiran at paulit-ulit na puna ng tao. Nagawa ng sistema na hatiin ang mahirap na tanong sa mas maliliit na gawain, magsiyasat ng ilang direksiyon at magbalik ng mga resulta upang suriin ng mga mananaliksik.

Pinagsama ng paraan ng pagsasanay ang malawak na kaalamang siyentipiko at materyal na nakatuon sa matematikal na pananaliksik, kabilang ang mahihirap na problemang mula sa mga papel matematikal at mga paraang ginagamit upang suriin ang mga iminungkahing solusyon. Inilarawan din ng laboratoryo ang reinforcement learning gamit ang mga beripikableng gantimpala, ibig sabihin, maaaring magsilbing hudyat sa pagsasanay ang matagumpay at masusuring pangangatwiran.

Pagkatapos, ginamit ng mga mananaliksik ang karanasang mula sa pansuportang sistema upang pahusayin ang mismong modelo. Praktikal na layunin nitong mapanatili ang kapaki-pakinabang na pag-usad sa mahabang pagsisiyasat, kabilang ang pagsubaybay sa mga pansamantalang resulta at pagtutuwid ng mga pagkakamali habang umuunlad ang mga bagong argumento.

Bumanggit din ang laboratoryo ng mga resulta sa IMO-Proof at AdvancedMathBench, mga pagsusuring nakatuon sa pangangatwirang matematikal. Para sa proyektong Ghys, ang pinakadetalyadong ebidensiya kung paano gumana ang sistema ay ang sunod-sunod na malawak na derivation, puna ng mga eksperto, natapos na papel at kasunod na pormal na beripikasyon.

Paano sinuri ng Peking University ang patunay

Ginamit ng pangkat ng Peking University na pinamumunuan nina Bin Dong at Ruochuan Liu ang balangkas nitong SHEAF upang pormalisahin ang lahat ng apat na pangunahing teorema sa papel ni Zhang. Saklaw din ng gawain ang mga resultang nakuha ni Ghys na pinagbatayan ng mga argumento.

Isinasalin ng pormalisasyon ang mga depinisyon, palagay at pangangatwirang matematikal sa wikang kayang suriin ng kompyuter. Maaaring umasa ang isang karaniwang papel sa sinanay na mambabasang bubuo sa mga pamilyar na hakbang. Hinihingi naman ng Lean na ilahad ang mga hakbang na iyon sa pamamagitan ng mga tiyak na pahayag at pinahihintulutang lohikal na operasyon.

Ayon sa mga miyembro ng pangkat na sina Jiedong Jiang at Bin Wu, tumagal nang humigit-kumulang limang araw ang gawain at umabot sa 100 AI agent ang sabay-sabay na gumana. Nakabuo ito ng humigit-kumulang 550,000 linya ng Lean code. Sinuri rin ng mga eksperto kung tugma ang mga pormal na pahayag sa matematikal na kahulugan ng mga pangunahing teorema sa papel.

Isinaayos ng SHEAF ang gawain bilang directed graph ng mga depinisyon, proposisyon at dependency. Dahil dito, nagawa ng iba’t ibang agent na magtrabaho sa magkakaugnay na bahagi habang sinusubaybayan ng pangkat kung aling mga pahayag ang may patunay na at alin ang kailangan pang trabahuhin.

Hindi lamang pagsasalin ng mga huling argumento ang kinailangan sa pormalisasyon. Wala sa mga umiiral na pormal na aklatan ng matematika ang ilang pansuportang resulta sa dynamics. Kinailangan ng pangkat na buuin ang mga pundasyong iyon o humanap ng mga paraang gumagamit sa mga resultang naroon na, at pagkatapos ay pag-ugnayin ang mga bahagi bilang kumpletong hanay ng pangangatwiran.

Mababasa ang papel bilang paunang bersiyon sa arXiv, at inilabas sa GitHub ang pormalisasyong code. Walang binanggit sa anunsiyo tungkol sa pagkalathala sa journal o desisyon sa peer review.

Bakit magkaugnay ang dalawang yugto

Konkretong ipinakikita ng lawak ng gawain ang pagkakahating ito. Naging batayan ng isang papel-pananaliksik ang humigit-kumulang isang libong pahina ng eksplorasyong output; pagkatapos, nakabuo naman ang proseso ng beripikasyon ng mga 550,000 linya ng pormal na code. Hinubog ng bawat yugto ang gawain sa paraang angkop sa magkakaibang tungkulin.

Para sa mga susunod na mananaliksik, inilalahad ng pampublikong papel ang matematikal na argumento, habang itinatala naman ng pampublikong code ang estruktura ng pormal na patunay. Maaari ring magsilbing panimulang punto sa susunod na gawain sa larangang ito ang mga depinisyon at resultang idinagdag sa pormalisasyon.

Ang susunod na hakbang: isang muling magagamit na modyul ng beripikasyon

Planong gawing modyul ng matematikal na beripikasyon ng Shanghai AI Laboratory ang daloy ng trabahong ito para sa plataporma nitong Intern Duanyan para sa siyentipikong pagtuklas. Layunin nitong magamit muli sa mga susunod na proyekto ang kombinasyon ng pagsasaliksik ng modelo, puna ng eksperto at pormal na pagsusuri.

Nilalayon din ng laboratoryo na gamitin sa ibang disiplina na may kaugnay na estrukturang matematikal ang mga kakayahan sa pangangatwirang nalinang sa proyektong ito. Ang iminungkahing siklo ay lumutas ng problema sa pananaliksik, gawing muling magagamit na software ang mga kapaki-pakinabang na pamamaraan at gamitin ang mga ito sa isa pang pagsisiyasat.

Para kay Xu, pinalalawak ng resulta ang matagal na niyang interes sa pananaliksik sa pamamagitan ng pagtutulungan ng Great Bay University, Shanghai AI Laboratory, KTH at Peking University. Para sa mas malawak na komunidad ng matematika, nag-aalok ito kapwa ng bagong resulta sa klasipikasyon at ng detalyadong halimbawa ng paglahok ng AI sa pananaliksik sa ilalim ng paggabay ng tao.

Mahahalagang Punto

• Lulutas ng bagong patunay ang codimension-one case ng haka-haka ni Ghys, kabilang ang complex dimension three.
• Si Jiesong Zhang ang nag-iisang may-akda ng papel-pananaliksik, at sinabi niyang siya mismo ang nagsuri sa lahat ng matematika.
• Ginabayan nina Disheng Xu at Zhang ang Intern-S2 sa paulit-ulit na pagsasaliksik at pagbibigay ng puna.
• Lumaki ang problem graph ng modelo mula 15 node tungo sa 389, at umabot sa humigit-kumulang isang libong pahina ang mga derivation.
• Tumulong ang balangkas na SHEAF ng Peking University na pormalisahin sa Lean ang apat na pangunahing teorema at mga pansuportang resulta.
• Ayon sa ulat, tumagal nang humigit-kumulang limang araw ang pagsisikap sa beripikasyon at nakabuo ito ng mga 550,000 linya ng code.
• Plano ng laboratoryo na gawing modyul ng matematikal na beripikasyon na magagamit muli ang daloy ng trabahong ito.