AI-ul de la Axiom Math verifică teorema celor 246 de goluri dintre prime în Lean

Axiom Math spune că sistemul său AxiomProver a produs o demonstrație verificată de mașină în Lean 4 a celui mai puternic rezultat cunoscut privind golurile dintre numere prime: teorema conform căreia există infinit multe perechi de prime care diferă cu cel mult 246. Compania a publicat rezultatul pe 17 august 2026 ca un plan de formalizare interactiv creditat la 41 de contributori numiți în matematică, inginerie și ca investigatori principali, cu IEEE Spectrum a raportat prima dată această realizare.

Limita de 246 reprezintă marginea actuală a cunoașterii umane în atacul îndelungat asupra conjecturii gemenilor prime, ipoteza din secolul al XIX‑lea conform căreia primele separate exact prin doi apar la infinit. Pagina de proiect a Axiom Math descrie munca ca o formalizare unificată a lucrării lui James Maynard din 2013 „Small gaps between primes” împreună cu partea din continuarea colaborării Polymath8b care a restrâns limita lui Maynard de la 600 la 246. Demonstrațiile verificate de mașină sunt organizate într-o bibliotecă publică Lean, PrimeGapsLib, cu teorema de 246 ca rezultat principal.

„Această teoremă reprezintă în prezent pragul cunoașterii umane despre numerele prime”, a declarat Ken Ono, matematicianul fondator al Axiom Math.

Verificarea formală înseamnă traducerea unei demonstrații într-un limbaj pe care un program mic, de încredere, numit kernel îl poate verifica linie cu linie. Rezultatul nu este o garanție absolută — afirmația însăși trebuie tradusă corect, iar verificatorul trebuie să fie solid — dar elimină căderea în eroare a arbitrilor umani din lanț. Până acum, sistemele AI care concurează pe benchmark-uri de matematică au fost în mare parte evaluate pe probleme de competiție cu demonstrații scurte și auto‑conținute; diferența dintre acele rezultate și formalizarea la nivel de cercetare a fost largă, un model vizibil în sisteme anterioare care excelează la geometria olimpică în timp ce lăsau matematica de cercetare în mare parte neatinsă.

De la 70 de milioane la 246

Conjectura însăși, formulată precis de Alphonse de Polignac în secolul al XIX‑lea, rămâne ne demonstrată. Prima limită finită de orice fel a apărut în 2013, când Yitang Zhang a demonstrat că există infinit multe perechi de prime care se află la cel mult 70 de milioane una de alta. Câteva luni mai târziu, Maynard a introdus o metodă de sită rafinată și a redus limita la 600 — lucrare care a contribuit la Medalia Fields din 2022 — iar colaborarea Polymath8b, care l‑a inclus pe Maynard și pe Terence Tao, a împins limita la 246. Planul Axiom Math prezintă această progresie ca proiectul pe care a dorit să îl formalizeze.

Formalizarea urmează un flux de lucru pe care compania îl descrie în trei etape. Cercetătorii au scris mai întâi demonstrația ca un plan — fiecare definiție, lema și teoremă având o etichetă, o afirmație precisă și o listă a rezultatelor de care depinde — producând un grafic de dependență care a ordonat munca. AxiomProver, sistemul multi‑agent al companiei pentru cercetare matematică prin demonstrație formală, a generat apoi demonstrații Lean 4 verificabile de mașină, construite pe Mathlib, biblioteca comunității de matematică, și pe PrimeNumberTheoremAnd, proiectul de formalizare existent condus de Alex Kontorovich și Tao. Echipa Axiom a revizuit apoi codul generat și l‑a organizat în PrimeGapsLib.

Rezultatele principale declarate ale bibliotecii depășesc ușor teorema de titlu. Pe lângă limita de 246, aceasta formalizează limita de 600 a lui Maynard și include o provocare de verificare autonomă — construită doar pe Mathlib, cu slotul de demonstrație lăsat gol — care permite oricui deține instrumentul comparator Lean să confirme independent că demonstrațiile bibliotecii corespund teoremelor enunțate. Compania avertizează că verificarea completă poate dura ore; o versiune redusă care acoperă celelalte două rezultate rulează în minute.

Unde se încadrează aceasta în rândul revendicărilor de formalizare AI

Rezultatul apare într-un an de revendicări în creștere privind sistemele AI care efectuează matematică de nivel de cercetare, majoritatea ancorate pe scoruri de competiție sau demonstrații scurte. Axiom Math a fost unul dintre reclamanții mai agresivi: AxiomProver este creditat cu rezolvarea problemelor deschise anterior, inclusiv lucrări pe care compania le‑a publicat în reviste cu peer‑review, și sistemele AI au rezolvat acum mai multe probleme Erdős de lungă durată. Formalizarea de 246 este un tip diferit de rezultat — nu o teoremă nouă, ci o reconstrucție verificată de mașină a uneia dintre cele mai tehnic solicitante demonstrații din teoria numerelor modernă.

Comparația cea mai apropiată este de la începutul acestui an, când Math, Inc. a folosit agentul său Gauss pentru a finaliza demonstrația formală a rezultatelor de ambalare a sferelor ale lui Maryna Viazovska, câștigătoare a Medaliei Fields, în dimensiunile 8 și 24. Sidharth Hariharan, studentul doctorand de la Carnegie Mellon care a condus efortul uman de plan pentru acea formalizare și care este acum stagiar la Axiom Math și contributor matematic numit la proiectul de 246, susține că noul rezultat este realizarea mai cuprinzătoare. Raționamentul său, așa cum l‑a descris, este că Axiom a fost construit pentru reutilizare: în loc de o formalizare unică a unei singure demonstrații, PrimeGapsLib este o bibliotecă întreținută de rezultate privind golurile dintre prime, menită să susțină viitoare lucrări și cercetări de formalizare.

Această distincție contează pentru modul în care rezultatul ar trebui citit. O verificare unică demonstrează că un sistem poate rezista contactului cu o demonstrație dificilă. O bibliotecă demonstrează ceva mai apropiat de infrastructură — mașinărie formală reutilizabilă pe care alte rezultate o pot construi — care este direcția în care sistemele de demonstrație formală se îndreaptă pe măsură ce trec de la rezolvarea exercițiilor la verificarea matematicii reale. Afirmarea capacității aici se bazează pe artefacte care sunt publice și reexecutabile, nu pe un scor de benchmark: planul, codul Lean și o provocare comparator concepută astfel încât cercetătorii din afara să poată verifica singuri demonstrațiile.

Ono prezintă matematica ca un teren de testare pentru o ambiție mai amplă. Dacă proprietățile software‑ului — dacă un program se termină, dacă ieșirea sa este corectă pentru fiecare intrare — pot fi exprimate ca afirmații matematice precise, atunci sistemele derivate din AxiomProver ar putea să le demonstreze formal, susține el, îndreptându‑se spre verificarea codului generat de AI care începe să ruleze în infrastructuri, finanțe și sisteme de securitate.

„Lumea este pe cale să ruleze pe cod de calculator pe care nimeni nu l‑a citit”, a spus Ono. „AI este aici și nu mai putem închide ochii — formalizarea demonstrațiilor este un teren de testare pentru rezolvarea a ceea ce cred că este cea mai importantă provocare pe care o vom … … … …”

Pentru moment livrabilul este mai restrâns și verificabil: un plan de 41 de autori, o bibliotecă publică Lean și o demonstrație verificată de mașină că primele aflate la 246 una de alta nu se epuizează — cel mai apropiat vecin verificat al conjecturii gemenilor prime și cea mai profundă lucrare de matematică de cercetare pe care un sistem AI a verificat‑o până acum de la început până la sfârșit.