GPT-5.6 fant beviset som lukker et 30 år gammelt hull i konveks optimering

GPT-5.6 Sol Pro fant hovedargumentet i et matematisk bevis som lukker et 30 år gammelt hull i konveks optimering. Modellen brukte 148 minutter på oppgaven. Resultatet sier i praksis at Protasovs kjente metode fra 1996 allerede er omtrent så effektiv som mulig når en algoritme bare får se verdien av funksjonen den prøver å minimere – med unntak av logaritmiske faktorer.

Dette er ikke enda en benchmark der en AI-modell får noen prosentpoeng mer enn forrige modell. Det er et konkret forskningsresultat med et åpent bevis, full samtalelogg og maskinlesbar kontroll i Lean. Samtidig er arbeidet ferskt og ikke fagfellevurdert. Den siste setningen må være med, ellers blir dette reklame i stedet for journalistikk.

Det mest interessante er heller ikke at noen skrev en magisk setning og ventet i to og en halv time. Forskeren Phillip Kerger hadde arbeidet med problemet i omtrent ett år, prøvd eldre modeller uten å lykkes og samlet ti sider med faglig kontekst og forslag til angrepsmåter. Så traff en mye bedre prompt en modell som endelig var sterk nok. Det sier mer om fremtidens forskningsarbeid enn en overskrift om at «AI løste matte».

Hva var det 30 år gamle problemet?

Problemet handler om hvor mange forsøk en algoritme minst trenger for å finne en god løsning når den bare får spørre hva en funksjon er verdt i et valgt punkt. Protasovs algoritme fra 1996 har en øvre grense på O(d² log²(d+1)) funksjonsmålinger. Grovt sagt er det nær kvadratisk vekst med antall dimensjoner. Før det nye resultatet var den beste generelle nedre grensen ved den aktuelle nøyaktigheten bare i størrelsesorden d.

Bokstaven d er antall dimensjoner, eller enklere sagt antall variabler du kan justere. Tenk deg at du skal finne den beste kombinasjonen av temperatur, trykk og tid i en simulert produksjonsprosess. Du velger innstillinger, kjører simuleringen og får én kostnad tilbake. Du får ingen gradient som forteller hvilken retning du bør gå videre i.

Da oppstår et ganske grunnleggende spørsmål: Må algoritmen virkelig bruke nær kvadratisk mange målinger, eller har ingen bare funnet den smartere metoden som klarer seg med omtrent d? Kerger forklarer at Protasovs algoritme fra 1996 ga den nesten kvadratiske øvre grensen, mens den kjente nedre grensen ble stående lineær i tre tiår. GPT-5.6 fant argumentet som viser at den raske snarveien i hovedsak ikke finnes.

Hva beviste GPT-5.6 i konveks optimering?

Det nye resultatet gir en nesten kvadratisk nedre grense for deterministisk, derivatfri konveks optimering med eksakte funksjonsverdier. Mer presist utelukker det at en vilkårlig strategi kan garantere ønsket nøyaktighet med færre enn omtrent d²/log(d) spørringer. Det matcher den gamle øvre grensen opp til logaritmiske og konstante faktorer.

Det er en viktig presisering. Overskriften «d² er bevist nødvendig» er grei som en kort forklaring, men matematisk er resultatet ikke en ren eksakt d²-grense uten forbehold. Det åpne prosjektet oppgir blant annet en grense større enn d² delt på 1 800 log(d+1) i odde dimensjoner. I kompleksitetsteori er det likevel nok til å lukke den store forskjellen mellom lineær og kvadratisk avhengighet av dimensjonen.

Den første uavbrutte modelløkten løste den kvadratiske dimensjonsavhengigheten ved en nøyaktighet i størrelsesorden d^-3, selv om prompten ba om d^-4. En senere samtale ga den skarpere nøyaktigheten d^-1/2. Det er denne forbedrede deterministiske nedre grensen som nå er fullt representert i Lean-prosjektet.

Avgrensningen betyr også noe. Resultatet gjelder deterministiske strategier som får eksakte funksjonsverdier for konvekse, 1-Lipschitz-funksjoner på en euklidsk kule. Strategien kan ellers ha ubegrenset regnekraft og hukommelse. Beviset sier ikke automatisk det samme om tilfeldige algoritmer, støyende målinger eller alle praktiske optimeringsproblemer. Det gjør ikke resultatet mindre ekte. Det forteller bare hva som faktisk er bevist.

Hvor mye gjorde forskeren selv?

Phillip Kerger satte problemet, bygget den faglige rammen, skrev en prompt på omtrent ti sider, kontrollerte modellens argument og formaliserte resultatet i Lean. GPT-5.6 Sol Pro fant den avgjørende konstruksjonen og hovedargumentet i én uavbrutt økt på 148 minutter. Den ryddige beskrivelsen er derfor AI-assistert forskning, ikke en modell som våknet alene og valgte seg et problem.

Kerger er selv ekspert på nedre kompleksitetsgrenser. I den opprinnelige faglige redegjørelsen skriver han at han hadde arbeidet sporadisk med problemet i rundt ett år. Han hadde også forsøkt lange økter med GPT-5.4 og GPT-5.5 uten å komme i mål. Etter OpenAIs arbeid med Cycle Double Cover-problemet bygget han en mer omfattende prompt etter samme metodikk.

Det var altså mye menneskelig arbeid i forkant. Prompten inneholdt ideer om hvilke veier modellen burde prøve og hvordan den skulle arbeide. Men det er heller ikke rimelig å late som GPT-5.6 bare fylte inn et par manglende linjer. Kerger sier at modellen fant et hovedargument han selv ikke hadde klart å bevise, i et fagområde der han har jobbet nettopp med slike grenser.

For meg er denne fordelingen mer interessant enn en krangel om hvem som «egentlig» gjorde matematikken. En forsker kan bruke et år på å forstå problemet, pakke inn den riktige konteksten og kontrollere svaret. Modellen kan utforske og koble eksisterende teknikker i en fart mennesket ikke matcher. Når begge delene er nødvendige, har du en ny arbeidsform – ikke en ren konkurranse mellom menneske og maskin.

Hvorfor er Lean-verifiseringen viktig?

Lean kontrollerer at hvert logiske steg følger fra de formelle antakelsene. Prosjektet inneholder både utfordringsutsagn, løsning, sammenligningsoppsett og bygginstruksjoner. Produksjonsbevisene bruker ingen prosjektspecifikke aksiomer og ingen sorry eller admit, altså markører som lar et manglende bevissteg passere.

Dette er akkurat den typen kontroll AI-generert matematikk trenger. En språkmodell kan skrive et argument som høres imponerende ut, bruker riktige fagord og likevel skjuler et hull midt i beviset. Lean lar seg ikke sjarmere. Enten passer typene og slutningene sammen, eller så stopper kontrollen.

Verifikasjonsloggen fra 17. juli 2026 oppgir Lean 4.32.0 og Mathlib 4.32.0, beskriver kjøring med --trust=0 og viser hvilke standardaksiomer som er tillatt. Repositoryet skiller også uttrykkelig mellom den opprinnelige d^-3-varianten og den skarpere d^-1/2-varianten.

Men Lean er ikke en universell sannhetsmaskin. Den kontrollerer det formaliserte utsagnet, ikke om forskningsresultatet er nytt, betydningsfullt eller formulert på den mest naturlige måten. Prosjektet sier dessuten klart at Protasovs øvre grense og den samlede tosidige kompleksitetspåstanden ikke er formalisert der. Fagfellevurdering og kontroll av koblingen til litteraturen er fortsatt nødvendig.

Blir praktiske optimeringsverktøy bedre nå?

Nei, ikke direkte. Beviset leverer ikke en ny algoritme som gjør simuleringen eller maskinlæringen din raskere i morgen. Det viser at den kjente kvadratiske spørringskostnaden i denne strengt definerte modellen i hovedsak er uunngåelig. Det er en grense for hva du kan håpe å forbedre, ikke en ny knapp i et verktøy.

Slike grenser er likevel nyttige. De forteller forskere om det er verdt å lete videre etter en dramatisk raskere generell algoritme, eller om innsatsen heller bør flyttes til bedre antakelser, tilfeldige metoder, mer informative målinger eller spesielle problemklasser. Å vite at en dør faktisk er låst kan spare ganske mye tid på å riste i håndtaket.

Funksjonsverdi alene er dessuten et reelt scenario. Det dukker opp når en vurdering kommer fra en dyr simulator, et fysisk eksperiment eller menneskelig tilbakemelding. Men det bør ikke blandes sammen med all maskinlæring. Mange treningsmetoder har tilgang til gradienter, bruker stokastikk og arbeider med ikke-konvekse mål. Det nye beviset dekker ikke automatisk alt dette.

Den praktiske effekten i dag ligger derfor mer i forskning enn i programvare. Vil du prøve modellen i eget arbeid, er GPT-5.6 Sol tilgjengelig i ChatGPT, Codex og OpenAI API. Sol Pro-innstillingen Kerger brukte, er tilgjengelig for Pro- og Enterprise-brukere i ChatGPT. OpenAI beskriver modellen som sin sterkeste for å akselerere AI-forskning. Selskapets egne påstander er naturligvis markedsføring, men denne saken gir et langt mer interessant datapunkt enn enda en intern evaluering: en ekstern fagperson la fram problem, prompt, samtale og formelt kontrollert resultat.

Hva sier dette om AI og forskning?

Resultatet tyder på at mange åpne problemer ikke mangler helt ny matematikk. De mangler den riktige konstruksjonen, den riktige kombinasjonen av kjente teknikker eller rett og slett nok konsentrert letearbeid. Kerger mener selv at moderne AI kan ta problemer som lar seg løse med eksisterende verktøy, selv når frukten henger et godt stykke over bakken.

Det er en mer nøktern og samtidig mer omfattende påstand enn at GPT-5.6 er en digital matematiker som klarer alt. Modellen mislyktes ikke bare én gang i historien før gjennombruddet. Tidligere modellgenerasjoner kom ingen vei i lange økter. Først kombinasjonen av opparbeidet fagkontekst, en gjennomtenkt arbeidsmetode og en sterkere modell ga resultatet.

Dette passer også inn i en større utvikling der AI går fra å gjette raske svar til å arbeide lenge med etterprøvbare leveranser. Jeg har tidligere skrevet om hva som skjer når AI bruker mer tid på resonnement, og om GPT-5.4 og mer selvstendig verktøybruk. Her ser vi den samme retningen i forskning: langvarig arbeid betyr noe først når resultatet kan kontrolleres.

Så ja, dette ser ut som et ekte gjennombrudd innenfor den avgrensningen som er publisert. Nei, det betyr ikke at hele matematikken er ferdig til lunsj. Det betyr at en ekspert med ett års problemforståelse og en ti sider lang prompt fikk en modell til å finne et manglende bevis på 148 minutter – og at bevisets sentrale nedre grense kunne formaliseres og kontrolleres i Lean. Det er mer enn dramatisk nok uten å pynte på det.

Ofte stilte spørsmål