Las matemáticas siempre han dependido de dos lenguajes distintos. Uno es el lenguaje natural que usamos para explicar ideas, contar historias y compartir conocimientos; es flexible, rico en contexto y a menudo se salta pasos que parecen obvios para un lector humano. El otro es el lenguaje formal de los asistentes de pruebas, sistemas informáticos rígidos que verifican cada movimiento lógico para asegurar que una conclusión sea indiscutiblemente verdadera. Durante décadas, investigadores han trabajado en la traducción del primer lenguaje al segundo, un proceso llamado autoformalización. El objetivo era simple: tomar una prueba escrita por un humano y convertirla en código que una computadora pueda verificar. Pero un problema crítico persistía. Una computadora a menudo podía producir una prueba que era técnicamente correcta, pero que no guardaba semejanza alguna con el argumento humano que la inspiró. La computadora podía resolver el problema utilizando un camino completamente diferente, ocultando el razonamiento original tras un muro de atajos automatizados. Esto creó una brecha entre la verdad y la comprensión. Si la prueba de la computadora no sigue los pasos del humano, no podemos usarla para comprobar si el razonamiento del humano fue realmente sólido, ni podemos confiar en ella para enseñarnos cómo funciona el argumento.

Un equipo de investigadores ha abordado ahora esta brecha con un nuevo sistema diseñado para que la prueba de la computadora sea fiel al proceso de pensamiento original del humano. Lo llaman Pistis, un nombre derivado de la palabra griega antigua para fe o confianza. Los investigadores aplicaron este sistema a los tres primeros libros de los Elementos de Euclides, un texto fundacional de geometría escrito hace más de dos mil años. Su trabajo demuestra que es posible traducir estos argumentos antiguos a un lenguaje de computadora moderno sin perder la lógica original, al mismo tiempo que descubren errores ocultos en el texto que habían pasado desapercibidos durante siglos.

El desafío central que enfrentó el equipo fue que el lenguaje natural y la lógica computacional operan con ritmos diferentes. Una prueba humana podría decir: "Supongamos que esto es cierto", y continuar, esperando que el lector llene el vacío. Una computadora, sin embargo, exige que cada uno de los pasos sea explicitamente enunciado y justificado. Los intentos previos de traducir pruebas a menudo permitían que la computadora llenara estos vacíos con su propia lógica, reescribiendo efectivamente el argumento para facilitar la tarea a la máquina. El resultado era una prueba que compilaba con éxito pero fallaba en reflejar la intención del autor humano. Pistis fue construido para prevenir esto. En lugar de pedirle a la computadora que encuentre cualquier forma posible de probar el enunciado, el sistema obliga a la computadora a seguir el camino específico del humano, oración por oración.

Para lograr esto, los investigadores desarrollaron un método que divide el proceso de traducción en dos fases distintas. Primero, una fase de mapeo analiza el texto en lenguaje natural y lo divide en una secuencia de pasos pequeños y atómicos. Identifica exactamente qué afirma cada oración y en qué supuestos se apoya. Esto crea una plantilla estricta que la computadora debe seguir. Segundo, una fase de llenado intenta probar cada uno de estos pequeños pasos individualmente. El sistema utiliza una estrategia de búsqueda especializada que evita que la computadora tome atajos o se adelante. Si la computadora no puede probar un paso específico utilizando las herramientas y referencias exactas que menciona el texto humano, no se limita a encontrar otra forma de resolver el problema. En su lugar, señala el problema, revelando que el argumento humano original podría tener un hueco o una pieza faltante.

Este enfoque resultó ser notablemente efectivo cuando se probó en la geometría de Euclides. Los investigadores generaron pruebas formales para 92 proposiciones a través de los tres primeros libros. Cuando compararon estas nuevas pruebas con intentos anteriores, la diferencia fue contundente. Las nuevas pruebas compilaban más de treinta y tres veces más rápido, una mejora significativa en la eficiencia que sugiere que el nuevo método evita las computaciones pesadas y lentas de los sistemas anteriores. Más importante aún, los expertos humanos que revisaron las pruebas prefirieron la producción del nuevo sistema por un margen amplio. En un estudio a ciegas, los revisores encontraron que las nuevas pruebas eran mucho más transparentes y mejores representaciones de los argumentos del libro de texto original. Un juez de inteligencia artificial, entrenado para evaluar la calidad de la traducción, estuvo de acuerdo, favoreciendo las nuevas pruebas sobre las antiguas por una proporción de más de cinco a uno.

Más allá de simplemente traducir el texto, el sistema actuó como un verificador riguroso que expuso fallas genuinas en el material de origen. Debido a que el sistema insiste en seguir la lógica humana exactamente, no puede ocultar errores. En un caso, el sistema identificó un error de citación en una traducción moderna de Euclides. El texto referenciaba una proposición sobre cortar una línea a la mitad, pero la citación apuntaba a una proposición sobre cortar un ángulo. El sistema señaló este desajuste, mostrando que la traducción había vinculado la idea equivocada con el paso equivino. En otro caso, el sistema encontró un vacío en el propio razonamiento de Euclides donde un escenario específico quedó sin abordar. Los investigadores pudieron demostrar formalmente que el argumento original era incompleto, un descubrimiento que habría sido difícil de realizar sin una herramienta que se adhiera estrictamente a la estructura original.

El éxito de Pistis sugiere que la formalización fiel no es solo un ejercicio técnico, sino una poderosa herramienta para verificar el conocimiento humano. Al obligar a la computadora a caminar la misma senda que el humano, el sistema puede confirmar si el razonamiento se sostiene o dónde se rompe. Los investigadores encontraron que su método podía aceptar argumentos válidos, refutar los inválidos y señalar exactamente dónde falló una prueba. Esta capacidad se extiende más allá de la geometría antigua; el marco está diseñado para trabajar con cualquier argumento matemático escrito en lenguaje natural. El trabajo demuestra que no tenemos que elegir entre la flexibilidad de la explicación humana y el rigor de la verificación de la máquina. Es posible tener ambos, siempre que la máquina sea guiada para respetar la voz y la lógica originales del humano.

El estudio también destacó los límites de la tecnología actual. Aunque el sistema funcionó bien para los tres primeros libros de Euclides, no pudo manejar cada una de las proposiciones de los libros posteriores sin guía humana adicional. Algunas proposiciones requerían conceptos geométricos que el sistema informático subyacente aún no sabía cómo manejar, tales como medir la longitud de una línea curva. Los investigadores señalaron que su sistema depende de un humano o de una inteligencia artificial avanzada para actuar como un oráculo, verificando que el mapeo inicial del texto sea correcto. Esto significa que el proceso no es totalmente automático todavía, pero reduce significamente la cantidad de trabajo manual requerido en comparación con métodos anteriores.

En última instancia, el artículo presenta un nuevo estándar para cómo interactuamos con las pruebas matemáticas en la era de la inteligencia artificial. Va más allá de la pregunta de si una computadora puede probar un teorema hacia la pregunta más profunda de si la computadora entiende el argumento. Al asegurar que la prueba formal sea un espejo del argumento en lenguaje natural paso a paso, los investigadores han creado una herramienta que puede validar el razonamiento detrás de una conclusión, no solo la conclusión en sí. Esto permite que matemáticos y estudiantes confíen en que la computadora no solo está encontrando una solución, sino que está siguiendo verdaderamente la lógica de la persona que escribió la prueba. El trabajo ofrece un camino a seguir donde la visión humana y la precisión de la máquina trabajan juntas, preservando la integridad del descubrimiento matemático mientras se aprovecha el poder de la verificación moderna.