Fa mesos que els laboratoris d'IA anuncien que els seus models resolen problemes oberts de matemàtiques, i la comunitat matemàtica reclama que, abans de celebrar-ho, es pugui comprovar què s'ha demostrat de debò. A finals de setembre, un grup independent d'experts de l'Institut d'Estudis Avançats de Princeton va publicar recomanacions per a aquests anuncis, després de rebre més de 600 respostes de matemàtics.
El 6 d'octubre, OpenAI ha penjat al repositori públic openai/math, amb llicència Apache-2.0, 722 manuscrits agrupats en 372 famílies de resultats, que cobreixen matemàtica pura, informàtica teòrica i física matemàtica. Els ha produït un model intern que encara no ha estat llançat, a partir d'unes 4.000 preguntes; segons el fitxer de presentació, cada resultat va costar de mitjana l'equivalent a unes tres hores de còmput de ChatGPT Pro. La col·lecció diu que hi ha, entre altres afirmacions, una regió sense zeros per a les funcions L de Dirichlet, la conjectura de Mahler simètrica i un contraexemple a la conjectura dels divisors de zero de Kaplansky.
El que dona pes a la publicació és que 162 dels 722 articles porten una demostració formalitzada en Lean, un llenguatge que permet a un ordinador comprovar cada pas del raonament. Així, qualsevol matemàtic pot verificar aquests resultats sense haver de fiar-se de l'empresa. OpenAI també hi ha inclòs deu resums abreujats del raonament del model i ha reconegut públicament que alguns dels resultats no formalitzats «podrien tenir problemes».
Convé llegir-ho amb cautela. Els 560 manuscrits restants no tenen demostració comprovada per ordinador i el comunicat no parla de cap revisió independent; el model no és accessible, de manera que ningú no pot reproduir l'experiment, i l'empresa no ha publicat quantes de les 4.000 preguntes van quedar sense resposta. El grup d'experts de Princeton ja havia advertit que no avala que es provin problemes avançats amb models privats sense dir-ho, i demana que aquestes publicacions no es tractin com a màrqueting.