Startup-ul Axiom rezolvă două probleme Erdős cu Lean – AI-ul intră oficial în matematica pură

Două probleme notabile formulate de Paul Erdős , rămase nerezolvate timp de decenii, au fost formalizate recent de startup-ul Axiom folosind asistentul de demonstrații Lean , informează FineSkyAi . Problemele #481 și #124 , propuse în 1980 și respectiv în urmă cu aproximativ 30 de ani, erau considerate provocări serioase în domeniul matematicii pure. Axiom, companie specializată în integrarea inteligenței artificiale în cercetarea matematică, a reușit să demonstreze rigurozitatea soluțiilor printr-o formalizare completă în Lean – un sistem utilizat pentru verificarea logică a demonstrațiilor. Paul Erdős a formulat peste 1.100 de probleme de-a lungul carierei, din care doar aproximativ 266 au fost rezolvate până în prezent. Complexitatea acestora constă nu doar în conceperea întrebării, ci mai ales în lanțul subtil de raționamente logice necesare pentru a ajunge la o soluție validă. Soluțiile Axiom au atras atenția comunităților științifice, mai ales în contextul recentelor controverse legate de GPT-5. GPT-5: doar căutare, nu inovație Cu doar câteva săptămâni înainte, OpenAI susținea că modelul GPT‑5 ar fi rezolvat o serie de probleme formulate de Erdős. Însă, potrivit unor critici din mediul academic, aceste „demonstrații” nu erau originale, ci preluări din lucrări deja existente. Asta a stârnit o dezbatere în rândul matematicienilor privind ce înseamnă cu adevărat o descoperire matematică realizată de inteligența artificială: este suficientă corectitudinea, sau este nevoie de un proces logic nou și original? Surse precum TechBuzz au documentat reacțiile negative, subliniind importanța distincției dintre recuperarea informației și derivarea unor idei inedite. Axiom – un alt model de colaborare între AI și matematică Spre deosebire de cazul GPT‑5, Axiom nu doar că a produs soluții corecte, dar le-a și formalizat complet, în mod verificabil, folosind instrumente recunoscute în cercetarea academică. Lean este tot mai utilizat pentru demonstrații matematice formale, tocmai pentru că elimină erorile umane și confirmă pas cu pas validitatea fiecărei etape a raționamentului. Prin această abordare, Axiom reușește să se poziționeze nu doar ca un instrument de validare, ci ca un posibil partener în cercetarea matematică fundamentală . Experții apreciază că acest tip de colaborare între om și mașină – în care AI validează, structurează și extinde raționamente umane – ar putea deveni norma în viitorul matematicii. Spre o matematică asistată de AI Rezultatul celor de la Axiom este văzut ca un punct de cotitură: demonstrează că AI-ul poate depăși simpla replicare și poate contribui, prin mijloace formale, la progresul în matematică pură. Deși există încă voci sceptice privind creativitatea sistemelor automate, este clar că în zonele în care rigoarea este prioritară – precum demonstrațiile formale – AI-ul poate avea un rol de neînlocuit. Pe măsură ce tot mai multe universități integrează în pregătirea studenților instrumente precum Lean, se conturează o direcție clară: o matematică în care intuiția umană este completată de precizia mașinilor. Un viitor în care colaborarea contează Cazul Axiom arată că viitorul AI-ului în matematică nu înseamnă înlocuirea cercetătorului, ci colaborare. Este esențial ca sistemele automate să nu fie doar corecte, ci și capabile să ofere transparență și coerență în logica aplicată. Deocamdată, demonstrațiile complet automate rămân o raritate, însă exemple precum cele oferite de Axiom ne arată că procesul se accelerează. Chiar dacă soluționarea unor probleme vechi este un pas important, dezbaterea abia începe: ce înseamnă creativitate matematică? Poate AI-ul să intuiască și să generalizeze, sau doar să verifice? Aceste întrebări vor însoți, cel mai probabil, fiecare reușită viitoare din acest domeniu aflat într-o rapidă transformare. [...]