Els grans laboratoris d'intel·ligència artificial porten mesos competint per demostrar que els seus models no es limiten a aplicar matemàtiques ja conegudes, sinó que poden generar coneixement matemàtic genuïnament nou i verificable, un terreny on OpenAI, Google DeepMind i altres grups inverteixen sumes creixents des que els primers models de raonament van començar a resoldre problemes de competicions olímpiques i, més recentment, conjectures obertes.
Aquest 1 d'agost, OpenAI ha presentat Astra, una nova família de models pensada per a tasques llargues que exigeixen coordinar diversos agents, i n'ha mostrat les capacitats publicant deu demostracions de problemes matemàtics i de ciència de la computació que els especialistes no havien pogut resoldre en almenys una dècada, i en alguns casos molt més temps. Entre els resultats hi ha la prova de l'existència dels anomenats grups no sòfics -que refuta la conjectura de rigidesa de Connes-, noves fites en l'empaquetament d'esferes en dimensions altes, en la complexitat de circuits, en la teoria de reticles per a criptografia i en combinatòria extremal. Cada demostració s'ha formalitzat amb el llenguatge Lean, la qual cosa genera un certificat verificable automàticament, i OpenAI ha publicat també el raonament pas a pas que hi ha darrere de cada solució. Segons la companyia, els tocs necessaris per generar les deu respostes haurien costat uns 2.000 dòlars als preus de l'API del seu model Sol.
La notícia és rellevant perquè la verificació automàtica amb Lean elimina el dubte, habitual en aquests anuncis, que les demostracions siguin plausibles però incorrectes: un certificat verificat per una màquina no depèn del criteri d'un revisor humà. Que alguns d'aquests problemes portessin més d'una dècada sense avançar-hi intensifica la competència amb Google DeepMind, que ja fa temps que persegueix objectius similars amb el seu sistema AlphaProof, i situa Astra com una nova classe de model, en paral·lel a les famílies Sol, Terra i Luna d'OpenAI.
Un investigador de la companyia, Noam Brown, ha reconegut que van intentar sense èxit alguns dels problemes del mil·lenni, i que en cada un dels deu casos publicats "no hi van dedicar gaire" càlcul, cosa que suggereix que encara es podria aprofundir molt més augmentant el temps de còmput per problema. OpenAI tampoc ha confirmat cap data de llançament per a Astra ni si arribarà com a GPT-6 o com una variant de la família GPT-5, de manera que es tracta, de moment, d'una demostració de capacitats i no d'un producte disponible.