course
Pe 1 august, OpenAI a publicat un raport susținând că următorul său model, numit intern Astra (încă indisponibil), a produs rezultate noi pentru zece probleme deschise diferite din matematică. (Nu, nu sunt problemele Millennium Prize, dar sunt semnificative oricum.)
Ce e remarcabil: aceste soluții nu reprezintă un progres incremental asupra problemelor; sunt rezolvări reale, verificate cu Lean. (Lean este un limbaj de programare și un asistent de demonstrații care forțează detalierea fiecărui pas al unui argument matematic într-o formă lizibilă de mașină.)
E mult de digerat dintr-odată. În acest articol, am organizat problemele pe domenii și descriu la nivel înalt ce s-a întâmplat, ce ar putea însemna asta pentru matematică, ca domeniu, și ce altceva putem afla despre Astra.
Care sunt cele zece probleme?
Iată fiecare rezultat, pe înțelesul tuturor, împreună cu domeniul specific de matematică sau informatică de care aparține.
Grupuri non-sofice
Domeniu: Teoria grupurilor
Astra a produs o construcție explicită a unui grup care nu poate fi aproximat, oricât de fin, prin structuri finite mari — închizând o întrebare deschisă de când a fost introdus, în 1999, conceptul de grup „sofic”. Construcția vine cu o demonstrație că nicio succesiune de aproximări finite nu poate funcționa vreodată, formalizată în Lean astfel încât logica să poată fi verificată mecanic.

Wikipedia a fost deja actualizată:

Împachetarea sferelor
Domeniu: Geometrie în dimensiuni înalte
Întrebarea este cât de dens pot fi împachetate împreună sfere identice, care nu se suprapun, pe măsură ce crește numărul de dimensiuni. Astra a demonstrat un plafon mai strâns pentru această densitate în dimensiuni înalte, prima îmbunătățire a acestei borne specifice din 1978. Nu oferă o metodă mai bună de împachetare — reduce intervalul a cât de bună ar putea fi orice metodă viitoare.
Coduri binare și sferice
Domeniu: Teoria codării
Codurile corectoare de erori funcționează păstrând mesajele valide suficient de departe unele de altele, astfel încât erorile mici să nu poată transforma un mesaj în altul. Astra a demonstrat limite mult mai strânse (îmbunătățite exponențial) asupra numărului de astfel de mesaje care pot exista pentru o distanță minimă dată, cu un rezultat corespunzător pentru puncte distribuite pe o sferă de dimensiuni înalte.
Conjectura de rigiditate a lui Connes
Domeniu: Algebre de operatori
Alain Connes a emis ipoteza că anumite grupuri ar putea fi întotdeauna reconstruite în mod unic dintr-o structură algebrică, numită algebră von Neumann, construită din ele. Astra a infirmat acest lucru, producând două grupuri cu adevărat diferite care dau naștere aceleiași algebre, arătând că reconstrucția nu este întotdeauna unu-la-unu.
Complexitatea circuitelor aritmetice
Domeniu: Teoria complexității computaționale
„Permanentul”, un singur număr calculat dintr-o grilă de numere, este costisitor de calculat, iar teoreticienii complexității vor să știe numărul minim de pași aritmetici de care ar putea avea nevoie orice metodă. Astra a demonstrat o nouă limită inferioară, mai puternică, asupra acestui minim — un tip de rezultat notoriu de greu de mișcat măcar puțin.
Repetiție paralelă cuantică
Domeniu: Teoria complexității cuantice
Teoria clasică spune că, dacă îi faci pe doi jucători care nu comunică să repete un joc dificil de multe ori în paralel, șansele de a trișa cu succes scad exponențial. Astra a demonstrat că aceeași garanție se menține chiar și când jucătorii împărtășesc încurcare cuantică, extinzând un principiu clasic fundamental la contextul cuantic.
Problema celui mai apropiat vector
Domeniu: Criptografie bazată pe rețele (lattices)
Dată o grilă repetitivă de puncte (un lattice) și o locație țintă, problema cere cel mai apropiat punct al grilei — o problemă considerată foarte grea în dimensiuni înalte, motiv pentru care stă la baza unor scheme de criptare rezistente la cuantic. Astra a demonstrat că chiar și aproximarea răspunsului, în limita unui factor polinomial specific, rămâne demonstrabil dificilă, consolidând criptografia construită peste ea.
Conjectura volumului lui Ehrhart
Domeniu: Geometrie discretă și convexă
Pentru o formă convexă al cărei unic punct interior al grilei se află exact în centrul de masă, matematicienii au vrut să știe cel mai mare volum posibil pe care o astfel de formă îl poate avea într-o dimensiune dată. Astra a determinat acel volum maxim pentru fiecare dimensiune, rezolvând complet conjectura.
Numere Ramsey multicolore
Domeniu: Teoria Ramsey / combinatorică
Cu suficient de mulți oameni și suficiente categorii de relații între ei, ești, în cele din urmă, garantat să găsești trei persoane conectate toate prin aceeași categorie. Astra a demonstrat că mărimea minimă a grupului necesară crește mai repede decât orice rată exponențială fixă pe măsură ce numărul de categorii crește, rezolvând problema 183 a lui Erdős.
Conjecturi privind numerele extremale
Domeniu: Teoria grafurilor extremale
Această ramură a matematicii întreabă câte conexiuni poate avea o rețea evitând totuși anumite tipare mici, interzise. Astra a rezolvat două conjecturi înrudite aici, corespunzătoare problemelor 146 și 180 ale lui Erdős, stabilind cât de dense pot deveni astfel de rețele înainte ca acele tipare să devină inevitabile.
Fiecare dintre acestea a fost deschisă de cel puțin un deceniu; câteva au rezistat treizeci de ani sau mai mult, incluzând probleme la care au lucrat câștigători ai Turing Award din zona de CS teoretică.
Stai, un contraexemplu e genul „ușor” de demonstrație?
Cine sunt eu să spun ceva negativ aici, dar știu că asta e o întrebare sau reacție comună, mai ales din partea celor care știu ceva matematică.
Cel mai des auzi, ca tip de critică: câteva dintre aceste rezultate sunt contraexemple, mai degrabă decât teorie generală nouă. Ideea e importantă, deoarece un contraexemplu răspunde la o întrebare de tip da/nu, dar nu îți spune, de unul singur, de ce se rupe tiparul sau nu îți oferă o familie de obiecte similare de studiat în continuare, pe când altceva, cum ar fi o teoremă de clasificare sau o tehnică nouă, deschide mai multe uși.
Aș spune că această critică stă în picioare în general, dar nu funcționează ca respingere în bloc a întregului acestui lot de probleme. În primul rând, rezultatul despre grupurile non-sofice nu e o mică ajustare a unei aproape-soluții existente — este prima construcție de acest fel după 27 de ani în care nimeni nu avea una, iar tehnica din spatele ei se așteaptă să se generalizeze pentru a găsi și altele.
În al doilea rând, câteva dintre celelalte nouă rezultate, inclusiv limita pentru împachetarea sferelor și dificultatea CVP, nu sunt deloc contraexemple; sunt îmbunătățiri directe ale bornelor existente.
Ce rămâne nerezolvat
Câteva aspecte merită urmărite, pe măsură ce domeniul va diseca aceste rezultate în zilele, săptămânile și lunile următoare:
- Încă fără peer review. Acestea sunt verificate în Lean și revizuite informal de matematicieni care au văzut preprinturi, dar niciuna nu a trecut printr-un proces de jurnal cu arbitraj.
- Autoria este încă în negociere. OpenAI spune că își asumă responsabilitatea pentru manuscrise și formalizările în Lean, atribuind în același timp argumentele matematice în sine modelului. Replicarea independentă a procesului (spre deosebire de verificarea demonstrațiilor) este greu de realizat acum.
Ce înseamnă asta pentru matematică
Cea mai imediată schimbare ține de ceea ce ar putea face efectiv matematicienii cu timpul lor. Dacă o problemă deschisă bine formulată poate fi dată unui model și verificată în Lean, blocajul se mută de la „poate cineva să rezolve asta” la „am pus întrebarea potrivită și am formalizat-o corect”. Arta de a formula o problemă bună și de a ști care merită atacată este o abilitate reală pe care matematicienii o dezvoltă prin experiență.
Mai există și o chestiune de finanțare și credibilitate, care fierbe în fundal. Granturile de cercetare, dosarele de titularizare și premiile au fost construite istoric în jurul rarității: aceste probleme erau suficient de dificile încât rezolvarea uneia spunea ceva despre autor. Dacă rezultatele asistate de AI devin de rutină, domeniul va avea nevoie de modalități noi de a semnaliza ce e cu adevărat dificil față de ce e acum la îndemâna a câteva mii de dolari de inferență. Desigur, omul de rând nu înțelege pe deplin aceste probleme. Cei cu pregătire reală da, iar asta nu se schimbă. Deci cunoașterea matematică e mai valoroasă ca oricând.
Cum reacționează oamenii
Reacțiile din social media s-au împărțit mai puțin în privința verificării demonstrațiilor și mai mult în privința a ceea ce reprezintă acestea ca dovezi.
Unii văd chiar ritmul ca fiind povestea principală: zece probleme vechi de decenii rezolvate deodată, în domenii fără legătură, mai repede decât pot experții să le revizuiască. O întrebare pentru viitor: „Vom putea ține pasul cu verificarea tuturor acestora?”

Alții susțin că asta spune mai puțin despre AI, în general, decât pare. Matematica e un domeniu rar în care munca unui model poate fi verificată automat și complet. Majoritatea problemelor din lumea reală nu oferă un astfel de barem automat, încorporat. Din acest punct de vedere, realizarea e reală, dar poate spune mai mult despre faptul că matematica e neobișnuit de potrivită pentru AI.

Un al treilea fir al comentariilor: o demonstrație corectă pe care nimeni nu a auditat-o sau asimilat-o pe deplin nu a fost încă înțeleasă, ci doar verificată. Descoperirea unei teoreme și înțelegerea a ceea ce înseamnă, din această perspectivă, sunt două lucruri diferite.

Gânduri finale
Matematicienii spun că rezultatul despre grupurile non-sofice pare autentic: o întrebare deschisă, veche de decenii, în teoria grupurilor, închisă printr-o construcție explicită pe care matematicienii din domeniu o iau în serios. Celelalte nouă rezultate, luate împreună, reprezintă un lot larg și substanțial tehnic de progres în matematica pură.
Ce nu s-a întâmplat încă este partea mai lentă: peer review, replicarea procesului de căutare și faptul că domeniul chiar construiește peste aceste rezultate. Acea parte durează mai mult decât un articol de blog și este partea care ne va spune cu adevărat cât de mare a fost acest moment. Te ținem la curent.
Întrebări frecvente
Întrebarea despre grupurile non-sofice este acum complet închisă?
Da, în sensul că acum există un exemplu valid, verificat în Lean. Programul mai amplu de cercetare — găsirea altor grupuri non-sofice și înțelegerea a ceea ce le face non-sofice — abia începe.
Au trecut aceste rezultate prin peer review?
Nu. Rezultatele sunt verificate în Lean și au fost revizuite informal de matematicieni care au văzut preprinturi, dar niciuna nu a trecut încă printr-un proces formal de jurnal cu arbitraj.
Cum a fost calculată suma de 2.000 $, și acoperă și încercările eșuate?
OpenAI spune că reflectă costul în tokeni al generării celor zece soluții publicate. Nu include însă câte alte probleme ar fi putut încerca Astra și pe care nu le-a rezolvat pe parcurs, deci nu este un cost total al cercetării, ci doar costul reușitelor.
Ce garantează de fapt „verificat în Lean”?
Garantează că pașii logici dintr-o demonstrație sunt intern coerenți și decurg corect unii din alții, deoarece compilatorul Lean nu acceptă un pas care nu corespunde. Nu confirmă independent că problema a fost formalizată astfel încât să însemne ceea ce au intenționat matematicienii, lucru pe care recenzorii umani trebuie încă să îl verifice.
Este vreunul dintre cele zece rezultate mai important decât celelalte?
Cei mai mulți matematicieni care s-au pronunțat indică drept remarcabilă construcția grupurilor non-sofice, având în vedere cât de mult a stat întrebarea deschisă și cât de centrală este pentru teoria grupurilor. Câteva dintre celelalte, precum problema celui mai apropiat vector și rezultatele despre împachetarea sferelor, sunt de asemenea văzute ca substanțiale, nu incidentale.