Resolver problemas matemáticos de élite no equivale a comprenderlos. Esa es la tensión central que emerge del análisis más reciente sobre el uso de modelos de inteligencia artificial en investigación matemática avanzada, y que pone en cuestión la forma en que los laboratorios tecnológicos comunican sus avances en este campo.

Un grupo asesor alojado en el Instituto de Estudios Avanzados de la Universidad de Princeton —integrado por investigadores de instituciones de primer nivel a escala global— publicó directrices específicas para laboratorios que trabajan en resolución de problemas matemáticos complejos. Entre sus recomendaciones principales: evitar el uso de modelos propietarios en estos ejercicios, formalizar las pruebas para que sean verificables por la comunidad, y liberar información sobre el proceso de razonamiento de los modelos. El cumplimiento de estas pautas ha sido parcial.

Formalización incompleta y opacidad en el razonamiento

De 719 documentos publicados en el marco de evaluaciones recientes, solo diez incluyeron liberaciones de la cadena de pensamiento —el registro del proceso interno de razonamiento del modelo—. Adicionalmente, apenas el 42% de las pruebas publicadas habían pasado por un proceso de formalización matemática, requisito considerado indispensable para que la comunidad científica pueda evaluar su validez con rigor.

Esta brecha no es menor. La formalización matemática no es un trámite burocrático: es el mecanismo que permite distinguir una solución correcta de una que solo parece correcta en lenguaje natural. Sin ese paso, los resultados quedan en un limbo verificacional que la comunidad matemática no puede —ni debe— aceptar como evidencia.

El problema estructural: lenguaje natural versus código verificable

Un estudio de investigadores de la Universidad de Cambridge y el King's College de Londres identificó una falla metodológica de fondo. Los modelos de IA generan primero una explicación en lenguaje natural y luego intentan traducirla a Lean, un lenguaje de programación diseñado para verificar la precisión formal de las pruebas. El problema: existen discrepancias significativas entre ambas representaciones, lo que significa que la prueba en lenguaje natural y su versión en código Lean no siempre describen lo mismo.

Esta desconexión tiene implicaciones directas para cualquier organización que esté evaluando el uso de IA en procesos que requieren precisión formal —desde auditoría financiera hasta modelado de riesgos o validación de algoritmos críticos—. La capacidad de un modelo para generar una respuesta plausible no garantiza que esa respuesta sea verificable ni reproducible bajo estándares rigurosos.

La pregunta sobre responsabilidad y financiamiento

Más allá de los aspectos técnicos, el debate abre una discusión sobre responsabilidad institucional. El grupo asesor ha propuesto que los laboratorios consideren financiar el trabajo de matemáticos humanos que puedan interpretar, contextualizar y validar los hallazgos generados por IA. Sin ese puente humano, los resultados corren el riesgo de quedar desconectados del ecosistema científico que les daría sentido y aplicabilidad.

Un matemático consultado en el marco de este análisis señaló que los modelos resuelven problemas de forma autónoma sin un interés genuino en el campo una vez que el problema inicial ha sido procesado. Esa desconexión —entre la capacidad de generar una solución y la capacidad de integrarse en una conversación científica continua— representa el límite más relevante de la IA aplicada a investigación de frontera en este momento.