El martes 6 de octubre, OpenAI publicó resultados matemáticos producidos por un modelo interno y abrió un repositorio para examinarlos. Al consultar el catálogo el 9 de octubre, aparecían 719 manuscritos agrupados en 372 familias; alrededor del 42% de los resultados principales tenía formalización en Lean. OpenAI los presenta en distintas etapas de verificación y dice que añadirá formalizaciones a medida que las obtenga. La cifra describe una colección cambiante, no una serie uniforme de resultados ya certificados.
Lean es un lenguaje para expresar definiciones, teoremas y demostraciones de modo que un programa pueda comprobar si una prueba se sigue de esas reglas y de los resultados incorporados al proyecto. El verificador no lee una explicación como la leería una persona. Comprueba una derivación formal. Si acepta la prueba, tenemos algo importante: una ruta inferencial codificada que satisface una formulación precisa, bajo las definiciones, resultados previos y axiomas que se hayan importado.
Formalizar una demostración puede detectar huecos, fijar con exactitud qué se ha probado y permitir que otros vuelvan a comprobarlo. El certificado tiene un objeto preciso: una proposición expresada en el sistema formal, junto con las definiciones, resultados previos y axiomas importados. La documentación de Lean explica que el verificador comprueba si la prueba se sigue de esos elementos; establecer que la formulación corresponde al problema matemático del manuscrito requiere un examen adicional de las definiciones y las bibliotecas utilizadas.
La precisión del verificador no identifica, por sí sola, a quien comprende la estrategia, puede explicar por qué funciona o sabe qué cambia al modificar una hipótesis. Comprobar una derivación formal y entender qué demuestra son logros distintos. Lean puede cerrar con exactitud la primera cuestión; la segunda depende de que alguien pueda dar cuenta del argumento y de su alcance.
Cuatro funciones que ahora se separan
En la práctica matemática, varias funciones suelen viajar juntas. Alguien propone un argumento, lo escribe, responde preguntas sobre sus pasos y defiende qué se sigue de él. La publicación deja un objeto que otros pueden revisar; su autoría identifica también a personas a quienes la comunidad puede interpelar. No siempre el autor domina cada detalle de una prueba extensa, y la matemática conoce argumentos colectivos, verificación asistida y resultados que solo se comprenden gradualmente. Lo que importa es que las tareas puedan distribuirse sin desaparecer.
La inteligencia artificial separa esas funciones con nitidez. Un modelo puede producir un argumento; una formalización puede certificar una derivación; una matemática puede apropiarse de la prueba al comprender su estructura y poder explicarla; una persona o institución puede responder por su publicación. Son cuatro trabajos distintos: producir, certificar, comprender e imputar responsabilidad. Imputar, aquí, significa atribuir quién debe corregir el registro y asumir responsabilidad editorial. Esa atribución no demuestra que alguien pueda reconstruir el argumento o valorar una objeción matemática sustantiva.
El repositorio de OpenAI vuelve visible la separación. La empresa declara que la colección incluye resultados en diferentes etapas de verificación, que no todos tienen formalización Lean y que algunos resultados aún sin formalizar podrían contener problemas. También conserva revisiones y versiones. Junto al catálogo publicó diez resúmenes abreviados del razonamiento del modelo: aportan una explicación sobre resultados seleccionados, no una transcripción exhaustiva del proceso de cada manuscrito. “Publicado”, “formalizado” y “verificado por expertos” describen estados diferentes; distinguirlos permite saber qué muestran los materiales disponibles y qué queda por examinar.
La validez de una prueba y la comprensión de su método responden a preguntas diferentes. Una máquina puede haber encontrado una demostración correcta cuya idea aún no se ha vuelto transparente para los matemáticos; la corrección sigue en pie. Lo que queda limitado es otra cosa: cuánto podemos afirmar sobre la explicación, la fecundidad del método y la posibilidad de reutilizarlo.
La diferencia entre acertar y enseñar
Una demostración puede aportar más que el establecimiento de su conclusión. Puede revelar por qué una conjetura era cierta, qué estructura escondía y qué problemas vecinos quedan ahora al alcance. Si una comunidad comprueba el resultado sin poder reconstruir la ruta, sabe que la conclusión se sostiene y aún puede ignorar qué principio general conviene aprender. El hallazgo añade un punto al mapa; la comprensión puede convertirlo en camino.
Esta diferencia no exige leer la mente del modelo. Se puede examinar públicamente si un sistema —o el equipo responsable— explica el papel de cada hipótesis, localiza el paso que falla al retirar un lema, adapta la prueba a una condición más débil y distingue qué conclusión sobrevive. La prueba consiste en observar si responde a variaciones pertinentes y mantiene continuidad entre la objeción, la explicación y la revisión.
OpenAI publicó diez resúmenes abreviados del razonamiento del modelo, referidos a resultados seleccionados. Pueden orientar al lector, y su alcance importa: no son transcripciones exhaustivas de cada proceso. Para saber qué acreditan sobre la comprensión de un argumento, habría que someter cada explicación a variaciones: cambiar una hipótesis, retirar un lema y preguntar qué conclusión sobrevive. La respuesta tendría que seguir la estructura de la prueba. El mismo examen vale para las personas: la autoría humana no certifica que el autor comprenda cuanto firma.
La imputación institucional cubre otra parte del asunto. OpenAI puede responder por los procedimientos de selección, edición, atribución y corrección de la colección. Esa obligación tiene consecuencias: mantener versiones, documentar cambios, ofrecer materiales revisables y corregir errores. La responsabilidad editorial identifica quién debe hacerse cargo de la publicación; la comprensión identifica quién puede exponer las razones matemáticas de una prueba. Una institución puede ejercer la primera sin que ello demuestre que un agente específico domina el método.
Qué debería significar publicar
La publicación de IA matemática mejoraría si cada resultado indicara con precisión su estado: manuscrito disponible, revisión matemática realizada, formalización Lean incluida, alcance de esa formalización y cuestiones que siguen abiertas. El porcentaje global sirve para describir la colección; no sustituye la ficha de cada teorema. Para una formalización concreta, importa saber qué enunciado verifica, qué definiciones e importaciones usa y si cubre el resultado central o solo un componente.
A esa ficha convendría añadir la historia de las revisiones y una explicación que permita a otros probar el argumento bajo cambios controlados. Si el equipo puede mostrar por qué una hipótesis es necesaria, qué parte del razonamiento se adapta a un caso vecino y dónde deja de funcionar, el resultado gana algo que el certificado nunca prometió: comprensión transferible. Si no puede hacerlo todavía, la descripción honesta es más limitada y no menos interesante: una derivación formalmente comprobada, con su alcance matemático y su interpretación aún bajo examen.
OpenAI dice que quiere que sus resultados impulsen la frontera del conocimiento y financiará encuentros dedicados a comprenderlos. Para que ese propósito se cumpla, esos encuentros deben ayudar a determinar qué está demostrado, cómo la formulación formal corresponde al problema matemático y qué pueden confirmar los matemáticos independientes. Hacer accesibles los resultados no consiste solo en subir archivos: exige explicar el alcance de cada formalización y dejar que otros examinen, corrijan y prolonguen el trabajo.
El certificado puede guardar intacta una demostración y permitir que cualquiera la vuelva a comprobar; por sí solo, no identifica a quien puede contestar por sus razones. Esa capacidad se muestra al explicar, aceptar variaciones, corregir y decir qué se aprende del resultado. En la matemática automatizada, el verificador ya puede cerrar una prueba. La tarea que queda abierta es hacer comprensible qué demuestra y quién puede explicarlo.