Lean-verifisert bevis skal ha lukket Ghys-formodningen fra 1995
Shanghai AI Laboratory kunngjorde 15. oktober 2026 at et forskerteam som jobbet tett med laboratoriets store språkmodell Shusheng-S2 skal ha lukket den tredimensjonale Ghys-formodningen – et problem innen kompleks dynamikk som har vært åpent siden 1995. Det som i så fall løfter saken over ren kunngjøring, er et formelt bevis i Lean-verktøyet der hvert logisk steg skal være maskinverifisert, og at den formaliserte koden er offentlig tilgjengelig. Men historien hviler foreløpig på laboratoriets egen annonsering: ingen uavhengig bekreftelse fra matematikermiljøet er dokumentert i det tilgjengelige kildematerialet.
Hva formodningen handler om
Den tredimensjonale Ghys-formodningen ble fremmet av den franske matematikeren Étienne Ghys i 1995, og har ifølge dekningen ligget ved fronten av komplekse dynamiske systemer siden. Det nye resultatet, publisert som preprint 2609.37695 (innsendt 29. september 2026, revidert 5. oktober 2026), avkler ifølge rapporteringen kodimensjon-én-tilfellet: holomorfe Anosov-diffeomorfier på kompakte komplekse tremangfold (MSN-dekningen; lenken går til sekundær dekning av preprinten, ikke til arXiv selv).
For ikke-matematikere kan dette omsettes grovt: Anosov-dynamikk beskriver systemer der baner med små avvik ekspanderer og kontraherer i kontrollerte retninger – en form for kaotisk men strukturert bevegelse. Ghys' formodning handler om når slike systemer eksisterer i den komplekse, holomorfe settingen, og tremangfold-tilfellet har vært en av de gjenstående bitene. Detaljene i beviset, og den presise betydningen av «kodimensjon én» i denne sammenhengen, kan ikke vurderes ut fra det tilgjengelige kildematerialet – det som rapporteres, er rekkevidden: holomorfe Anosov-diffeomorfier på kompakte komplekse tremangfold.
Hvem står bak
Arbeidet ble organisert rundt Xu Disheng, professor ved Great Bay University i Dongguan og gjesteforsker ved Shanghai AI Laboratory, og Jiesong Zhang, postdoktor ved KTH Royal Institute of Technology i Stockholm. Zhang tok doktorgraden under Xu ved Peking-universitetet og er eneste forfatter på artikkelen, ifølge MSN-dekningen.
En detalj verdt å merke seg: selv om modellen får mye av oppmerksomheten, er det et lite menneskelig team på to personer som står bak selve forskningsarbeidet. Det er altså ikke et eksempel på at en modell selv løser et matematisk problem, men på et tett menneske-maskin-samarbeid – og det er slik laboratoriet selv presenterer det.
Slik beskrives arbeidsmetoden
Arbeidet begynte i august 2026. Tilnærmingen var sentrert rundt Shusheng-S2 og laboratoriets spesialbygde «Harness system» – en plattform Shanghai AI Lab har utviklet for å støtte storskala rekursiv deduksjon og høybåndbredde-interaksjon mellom menneske og maskin. Det betyr, i den grad beskrivelsen lar seg tolke, at modellen ble brukt til å generere og utvide resonnementkjeder i stor skala, mens forskerne styrte og interpolerte i en tett iterativ sløyfe.
Her er en kildekonflikt som ikke kan løses ut fra tilgjengelig materiale: MSN-dekningen kaller modellen «Shusheng-S2», mens KuCoin-gjengivelsen av samme kunngjøring bruker varianter som «Shuwen-S2» og «Shuying-S2». Den mest detaljerte kilden er tydeligst og mest konsistent i navngivningen, så denne artikkelen følger «Shusheng-S2» – men lesere bør vite at navnet ikke er bekreftet mot laboratoriets egne primærkilder.
Verifiseringskjeden: det som faktisk er maskinsjekket
Det sterkeste leddet i historien er uavhengig av selve modellpåstanden: et team ved Peking-universitetet, med Dong Bin og akademiker Liu Ruochuan i spissen, skal ifølge kunngjøringen, gjengitt i KuCoins nyhetsflash, ha utført formell verifisering av beviset med sitt eget SHEAF-rammeverk og konstatert at det er korrekt. Beviset er formalisert i Lean, et bevissystem der korrektheten kontrolleres av en maskin, steg for steg, mot strenge formelle regler. Den formaliserte koden er offentlig tilgjengelig på GitHub, og preprinten ligger på arXiv.
Hva betyr det i praksis? Etter denne artikkelens egen vurdering sertifiserer en Lean-verifisering at den formaliserte versjonen av beviset følger av aksiomene uten logiske hull – en garanti som i styrke skiller seg fra tradisjonell fagfellervurdering, som ikke sjekker hvert logisk sted maskinelt. Men den sertifiserer ikke nødvendigvis at formaliseringen fanger det beviset hevder å bevise, og den sier ingenting om hvor betydningsfullt resultatet er. Og avgjørende her: det at et annet team skal ha kjørt verifiseringen, er foreløpig kun kjent gjennom laboratoriets egen kunngjøring. Koden er angitt som offentlig tilgjengelig, og det er derfor noe tredjeparter i prinsippet kan sjekke – men ingen slik tredjepartskontroll er dokumentert i kildene så langt.
Laboratoriets rammefortelling – og hva som er utsmykning
Shanghai AI Laboratory fremhever to poenger ut over selve matematikken. Det første er at resultatet ifølge laboratoriet viser verdien av et nytt vitenskapelig paradigme – altså en reproduserbar modell for menneske-AI-samarbeid i grunnforskning. Det andre, ifølge dekningen, er at dette angis som første gang en kinesisk stor modell bidrar til å løse en verdensklasse-formodning i ren matematikk.
Begge påstandene bør leses som selskapsutsagn, ikke etablerte fakta. Laboratoriet har en åpenbar interesse i å presentere sine modeller som vitenskapelig nyttige, og «paradigme»-språket er markedsføringens grammatikk mer enn matematikkens. Det samme gjelder «først»-påstanden, som ikke kan verifiseres ut fra tilgjengelige kilder. KuCoin-gjengivelsen inneholder dessuten en uforklarlig finansinnskrengning om «CFT og risikovillige aktiva», som ikke støttes noe steds og kan trygt se bort fra.
Hva som gjenstår før dette kan tas som et faktum
Saken er, med letsindig presisjon: sannsynligvis stor, men uavklart. Det viktigste å holde styr på:
- Ingen uavhengig bekreftelse. Det finnes ingen dokumentert validering fra det bredere matematikermiljøet av verken bevisets betydning eller Ghys-formodningens faktiske løsning. Lean-verifisering, hvis den sjekkes uavhengig, ville kunne endre dette raskt – det er hele poenget med formaliserte bevis.
- Primærdokumentene er ikke vurdert her. Både preprinten, GitHub-repoet og laboratoriets egen kunngjøring foreligger angivelig offentlig, men dekningen denne artikkelen bygger på er sekundære gjengivelser. Enkelte detaljer – som modellnavnet og «Greater Bay Area University» versus «Great Bay University» i KuCoin-versjonen – avslører at gjengivelsene har slurvefeil.
- Modellens rolle er uklar. Hvor mye av det matematiske arbeidet modellen bidro med, versus menneskene, beskrives ikke operasjonelt noe sted. «Storskala rekursiv deduksjon» er en arkitekturbetegnelse, ikke en redegjørelse for hva modellen faktisk bidro med i beviset.
Hvis Lean-koden sjekkes ut av uavhengige matematikere, vil dette uansett utfall være en milepæl verdt å notere: enten som bevis på at store modeller kan bidra i seriøs grunnmatematikk, eller som et eksempel på hvor raskt en «gjennombrudds»-fortelling kan løpe foran dokumentasjonen. Foreløpig er det kun det sistnevnte som er på det rene.