- Según el texto original, los resultados matemáticos generados por IA que OpenAI publicó suman unos 400 y abarcan más de 700 artículos. Incluyen varios campos, como la combinatoria, la geometría, la teoría de números y la informática teórica.
- OpenAI afirmó que formalizó en Lean unos 300 de los resultados clave de 719 artículos. Lean es un lenguaje de programación que ayuda a un ordenador a comprobar si una demostración es lógicamente correcta. El texto original lo describe como unos 42%.
- Los matemáticos señalaron que, aunque exista código en Lean, deben comprobar por separado si la demostración coincide realmente con las afirmaciones del artículo. Algunos artículos también recibieron críticas por tener listas de referencias breves y citas de fuentes insuficientes.
- El matemático de Stanford Jared Duker Lichtman valoró como importantes los avances hacia la hipótesis de Riemann, un caso particular de la conjetura de Hodge y resultados relacionados con la conjetura de Kakeya en 4 dimensiones. Se trata de la valoración de un investigador que habló con los periodistas, y el texto no confirma que la verificación de estos resultados hubiera terminado en el momento de la fuente.
Me llama la atención que haya un artículo con una lista de referencias corta. Para comprobar si se omitió alguna cita, al final hay que leer los manuscritos uno por uno, pero el artículo no deja claro quién revisaría los resultados cercanos a 400 ni en qué orden. Que 3 artículos se hayan retirado por un error de signo también sugiere que los resultados publicados no se pueden dar por definitivos de inmediato. Tengo curiosidad por saber cómo marcan el estado de verificación en su laboratorio cuando usan este tipo de material.