La versión interna del nuevo modelo Astra de la empresa OpenAI obtuvo diez resultados importantes en matemáticas. Los desarrolladores describieron estos logros como un avance significativo en geometría de altas dimensiones y teoría de códigos. La empresa publicó un extenso artículo con análisis detallados que explican el razonamiento de la red neuronal. Los investigadores también publicaron un repositorio especial con formalizaciones de todas las demostraciones en el lenguaje Lean 4. Los argumentos matemáticos fueron generados íntegramente por la versión interna del sistema, operando sin intervención humana directa. Las personas solo colaboraron con la red neuronal en la preparación de los manuscritos finales, entregándolos a la comunidad científica. Los representantes de OpenAI subrayaron la importancia de una atribución honesta al describir el proceso de obtención de resultados intelectuales. Atribuir la autoría a un humano distorsionaría la contribución real de la IA, que está desarrollando la ciencia moderna. El costo total de cómputo para encontrar las soluciones habría sido de aproximadamente dos mil dólares. Esta estimación no incluye la verificación posterior realizada por la comunidad matemática.
Uno de los resultados declarados se relaciona directamente con el problema de la repetibilidad paralela cuántica. Este concepto describe el cambio en la probabilidad de éxito al ejecutar repetidamente un juego interactivo. La red neuronal demostró la repetibilidad exponencial para juegos cuánticos finitos arbitrarios con dos participantes. Este resultado podría ser importante para el desarrollo de nuevos protocolos criptográficos. Otro logro se refiere al complejo problema de búsqueda del vector de red más cercano. El modelo obtuvo un resultado más sólido sobre la complejidad de la solución aproximada de este problema. El logro principal de la publicación de OpenAI es la construcción exitosa de un grupo no sofíco. Entre otros resultados se destacan estimaciones mejoradas para el empaquetamiento de esferas en altas dimensiones. Los investigadores también presentaron nuevas cotas inferiores en la complejidad de circuitos aritméticos. La empresa anunció el hallazgo de un contraejemplo a la conocida conjetura de rigidez de Connes.
La formalización de las demostraciones en el lenguaje Lean reduce significativamente el riesgo de lagunas lógicas habituales. El código publicado puede compilarse y verificarse fácilmente mediante métodos automatizados. Sin embargo, la verificación automática no reemplaza en absoluto una revisión científica completa. Los matemáticos aún deben evaluar la exactitud de la correspondencia entre los enunciados formales y los problemas originales. OpenAI citó expresamente la Declaración de Leiden, aprobada por la Unión Matemática Internacional. Este documento insta a mantener una atribución transparente al utilizar la IA en investigaciones. La empresa asume plena responsabilidad por la corrección de los materiales publicados. Al mismo tiempo, los propios argumentos matemáticos se atribuyen al sistema y no a los humanos. La publicación The Quantum Insider señaló la ausencia de una fecha de lanzamiento público del modelo Astra. Los desarrolladores aún no han puesto la red neuronal a disposición para pruebas independientes por parte de expertos externos.