OpenAI informó de cientos de resultados matemáticos producidos por un modelo de frontera interno, incluidas pruebas formalizadas en Lean y trabajos originales que abordan preguntas de investigación abiertas. La novedad tiene dos dimensiones: la cantidad de resultados propuestos y el uso de un asistente interactivo de pruebas para formalizarlos, lo que produce artefactos comprobables en lugar de simples argumentos en lenguaje natural. Esta combinación —razonamiento generativo y resultados verificables por máquina— es distintiva porque ofrece una vía para pasar de una idea inicial del modelo a algo que puede validarse mecánicamente, y permite una reproducción independiente más rápida que las afirmaciones basadas únicamente en texto.

Históricamente, los modelos de frontera se han evaluado por su capacidad para programar y resolver tareas lingüísticas; producir contenido matemático original los adentra en el terreno de la creatividad y la ciencia. El descubrimiento matemático requiere plantear conjeturas novedosas, construir argumentos sustanciales y sintetizar resultados existentes de formas que hagan avanzar el conocimiento. Cuando los modelos descubren lemas nuevos o completan lagunas en pruebas complejas, cumplen una función más parecida a la de un asistente de investigación que a la de una herramienta para desarrolladores. Este cambio transforma quién se beneficia de los resultados de los modelos y cómo los integramos: pasamos de programadores que aceleran la implementación a investigadores que agilizan la generación de hipótesis y la construcción de pruebas.

La formalización en Lean reduce la ambigüedad, pero no elimina el trabajo de verificación. Traducir una sugerencia informal del modelo a una prueba de Lean completamente especificada suele requerir trabajo de ingeniería humana: hay que elegir definiciones, codificar lemas y ajustar los scripts de prueba. Además, la formalización en Lean revela cadenas de dependencias y supuestos ocultos, pero también puede introducir errores propios. Por ello, un proceso sólido combina la comprobación automatizada de pruebas, repositorios reproducibles con versiones exactas del entorno y de la cadena de herramientas, y replicaciones independientes por especialistas que validen que la afirmación del modelo se sostiene más allá del artefacto inicial.

Los resultados matemáticos generados por IA obligan a las instituciones a revisar las convenciones de autoría y reconocimiento. Si un teorema se descubre con una ayuda considerable del modelo, ¿deberían figurar como autores el investigador principal humano, quien desarrolló el modelo, ambos o ninguno? Igual de importantes son los registros de procedencia: deben documentarse los scripts de prueba con control de versiones, los puntos de control del modelo, las instrucciones iniciales y las modificaciones humanas, para que quienes revisan el trabajo puedan seguir la evolución de una idea. Las revistas y conferencias deben actualizar sus políticas de presentación para exigir que se declare explícitamente la participación de modelos y definir cómo atribuir o rechazar afirmaciones originadas por IA cuando la procedencia no está bien documentada.

Los equipos deberían adoptar prácticas concretas: (1) tratar los resultados de los modelos como borradores que requieren formalización y verificación independiente; (2) mantener bajo control de versiones los scripts de prueba y registrar el modelo exacto y las instrucciones utilizadas; (3) establecer procesos de revisión interdisciplinarios que reúnan a especialistas del área e ingenieros de verificación; y (4) invertir en herramientas que automaticen la captura del entorno y la repetición de las pruebas. Las entidades financiadoras deberían priorizar proyectos que reduzcan la brecha de verificación y apoyar infraestructuras comunitarias que permitan reproducir las matemáticas asistidas por máquinas, en lugar de centrarse únicamente en ampliar los modelos o mejorar sus resultados en evaluaciones comparativas.