✨︎ Resumen (TL;DR):
- Stephen Wolfram advierte que una demostración validada por computadora puede responder una pregunta distinta de la original.
- AlphaProof y AlphaGeometry 2 resolvieron 4 de 6 problemas de la Olimpiada Internacional de Matemáticas de 2024 y obtuvieron 28 de 42 puntos.
- La fidelidad de la traducción se mide aparte de la comprobación, por lo que validar los pasos no garantiza conservar el sentido del enunciado.
Stephen Wolfram, creador de Mathematica, advierte que una demostración matemática validada por computadora puede responder una pregunta distinta de la original. En su ensayo del 28 de septiembre de 2026, examina qué implica automatizar la investigación matemática, sobre todo cuando la traducción del enunciado debe conservar sus condiciones y significado.
La autoformalización es un proceso que traduce las matemáticas escritas para personas a un lenguaje verificable por computadora. Ese paso exige conservar las condiciones y el significado del enunciado. Si la traducción los modifica, el sistema puede verificar una proposición distinta.
Lean separa buscar una demostración de comprobarla
La documentación de Lean distingue dos trabajos: encontrar una demostración y comprobarla. Este asistente permite definir objetos matemáticos, expresar afirmaciones y escribir pruebas con reglas precisas.
Para verificar una conclusión, cada paso debe apoyarse en definiciones, resultados anteriores o axiomas admitidos por el sistema. Las pruebas pueden expresarse como objetos completos, transferirse a otros sistemas y revisarse de forma independiente.
La automatización también ayuda a completar detalles que harían demasiado laboriosa una comprobación manual, según el manual de Lean. Pero esa capacidad no corrige una traducción que cambió la pregunta.
El ejemplo es sencillo. Demostrar que un número positivo tiene un cuadrado positivo no equivale a probar que cualquier número real tiene un cuadrado positivo. La segunda afirmación es falsa para cero. Si una traducción añadiera la condición de que el número sea positivo, produciría una proposición demostrable, pero habría modificado el enunciado original.
AlphaProof automatizó la búsqueda, no la traducción
Google DeepMind presentó el 25 de julio de 2024 un caso concreto de razonamiento automatizado. AlphaProof y AlphaGeometry 2 resolvieron 4 de los 6 problemas de la Olimpiada Internacional de Matemáticas de 2024 y obtuvieron 28 de 42 puntos, equivalentes al nivel de una medalla de plata.
Según el laboratorio, los problemas se tradujeron manualmente a lenguaje formal antes de que los sistemas buscaran las soluciones. La traducción inicial y la búsqueda de pruebas fueron etapas separadas.
Los estudiantes tuvieron 9 horas de competencia. Las herramientas necesitaron hasta 3 días para algunos problemas. AlphaProof combinaba un modelo de lenguaje con aprendizaje por refuerzo para producir demostraciones en Lean.
La fidelidad de la traducción se mide aparte
Un estudio aceptado en EMNLP 2025, encabezado por Auguste Poiroux, evaluó la corrección de las traducciones matemáticas. En el conjunto ProofNet#, GPT-4o pasó de 31.0% de acierto con una sola generación a 45.1% al producir 50 candidatos y aplicar filtros junto con una regla de selección.
El filtro de tipos descartaba enunciados mal formados en Lean antes de seleccionar una respuesta. La fidelidad al texto original se evaluaba por separado. Por eso, pasar ese filtro no equivalía a acertar la traducción.
Esos porcentajes miden la fidelidad de enunciados formalizados de nivel universitario en esa prueba, no la resolución general de problemas de investigación. El trabajo también analizó 619 pares de enunciados de investigación procedentes de 6 proyectos y encontró que el contexto del archivo, incluidas las definiciones locales, afectaba los resultados.
Los autores reconocen otra limitación: sus métricas dependen de formalizaciones de referencia correctas, que pueden faltar cuando se exploran matemáticas nuevas. Además, el estudio examina la traducción de enunciados, no la automatización completa de sus demostraciones.
La elección de las preguntas sigue en manos humanas
Para Wolfram, la imaginación humana sigue orientando qué preguntas investigar. La elección de objetivos sigue correspondiendo a las personas, aunque deleguen parte del trabajo técnico.
Lean puede revisar cada paso de una demostración formal, pero esa revisión no determina si el enunciado conserva la pregunta original. Verificar una demostración y conservar el sentido del problema son tareas distintas.
