En 2024, la Olimpiada Internacional de Matemáticas fue testigo de un hito histórico. Si bien la competencia es tradicionalmente una batalla de ingenio entre los estudiantes más brillantes del mundo, un participante no oficial se robó la atención: AlphaProof de Google DeepMind. El programa de IA obtuvo una puntuación de medalla de plata, lo que demuestra que las máquinas ya no se limitan a calcular números, sino que están empezando a dominar el arte del razonamiento lógico.
Este avance no es un milagro aislado de la ingeniería; es el resultado de una evolución de décadas en la forma en que verificamos la verdad a través del código. En su nuevo libro, La prueba en el código, el periodista Kevin Hartnett explora el improbable viaje de Lean, una herramienta de software que pasó de ser un asistente de codificación especializado a convertirse en la columna vertebral de la verificación matemática moderna y el desarrollo de la IA.
El puente entre el código y la lógica
La historia comienza con Leo de Moura, un ex ingeniero de investigación de Microsoft que lanzó Lean en 2013. Diseñado originalmente como una herramienta para verificar el código de software en busca de errores, el verdadero potencial de Lean residía en su similitud estructural con las matemáticas.
Como señala Hartnett, las dos disciplinas comparten un ADN fundamental:
– Sintaxis: Ambos requieren instrucciones precisas paso a paso.
– Lógica: Un solo error en una línea de código es funcionalmente idéntico a una “brecha” en una prueba matemática.
– Ejecución: Así como un programa sólo se ejecuta si la lógica es sólida, un teorema matemático sólo es válido si su demostración es hermética.
Esta comprensión provocó un movimiento. Si bien Lean no pudo “inventar” nuevas matemáticas por sí solo, actuó como un demostrador de teoremas interactivo. Podría ser necesaria una prueba escrita por humanos (que podría abarcar cientos de páginas y llevar meses revisarla por pares) y verificar su absoluta exactitud en un instante.
La lucha por un “lenguaje matemático”
La transición de las matemáticas tradicionales a la prueba digital no fue perfecta. Durante años, los matemáticos se enfrentaron al enorme problema del “huevo y la gallina”: para que Lean fuera útil, necesitaban vastas bibliotecas de definiciones matemáticas codificadas; pero para construir esas bibliotecas, necesitaban matemáticos que usaran el programa.
La fricción era a menudo absurdamente granular. Hartnett describe cómo el profesor Kevin Buzzard del Imperial College de Londres, mientras enseñaba a estudiantes universitarios, se encontró estancado porque Lean le exigió demostrar que 2 no es igual a 1. Para un humano, esta es una verdad obvia; Para un sistema lógico formal, es un hecho fundamental que debe definirse explícitamente antes de que pueda ocurrir cualquier razonamiento adicional.
Superar estos obstáculos requirió esfuerzos masivos de colaboración:
* Digitalización masiva: En 2018, los matemáticos pasaron meses traduciendo conceptos complejos como “espacios perfectos” en miles de líneas de código.
* Creación de comunidad: Un grupo pequeño y dedicado de investigadores trabajó para hacer que el software fuera fácil de usar, moviéndolo de una herramienta académica torpe a una plataforma sólida.
* Ampliación: Para 2025, el ecosistema se había disparado, con decenas de miles de usuarios de la academia y la industria tecnológica contribuyendo a las bibliotecas de Lean.
Por qué esto es importante: la búsqueda de una “máquina de la verdad”
La convergencia de las matemáticas y la IA es el objetivo final de este movimiento. Para ingenieros de software como de Moura, el premio fue una “máquina de la verdad” que podría garantizar que software como Microsoft Word esté completamente libre de errores. Para los matemáticos, es una forma de garantizar que incluso los descubrimientos más complejos y abstractos sean irreprochables.
Para los investigadores de IA, Lean sirve como el campo de entrenamiento definitivo. Al proporcionar una biblioteca masiva y verificada de verdades matemáticas, Lean permite que modelos como AlphaProof aprendan razonamiento riguroso en lugar de simplemente reconocer patrones. Esto es fundamental para resolver el problema de las “alucinaciones” en la IA: la tendencia de los modelos a expresar con seguridad información falsa. Si se puede entrenar a una IA para que siga las leyes estrictas e inflexibles de la lógica matemática, eventualmente podrá aplicar ese mismo rigor al razonamiento del mundo real.
“Tanto [matemáticas como codificación] están escritos con una sintaxis exacta como una serie de pasos lógicos, cada uno de los cuales conduce al siguiente”.
Conclusión
La prueba en el código narra cómo una herramienta especializada para la depuración de software se convirtió en la base de una nueva era de certeza matemática e inteligencia artificial. Destaca un cambio profundo en la ciencia: el movimiento hacia un futuro donde la intuición humana y la verificación digital trabajen en conjunto para definir lo que es verdad.
