El artículo «Can A.I. quicken the pace of math discovery?» presenta la iniciativa "Exponentiating Mathematics" de DARPA. Su objetivo es desarrollar una IA como coautor para acelerar la investigación en matemáticas.

El programa confronta limitaciones de los LLMs actuales. Estos fallan en razonamiento lógico-matemático y generan "alucinaciones". La solución propuesta integra IA con asistentes de prueba formales como Lean.

Lean desempeña el papel central como verificador. Los LLMs generan pruebas formales que Lean acepta o rechaza según su corrección. Esta iteración crea un ciclo de refinamiento continuo. Su lenguaje específico resulta arduo, pero su metodología es fundamental. La verificación formal garantiza corrección absoluta y elimina alucinaciones de LLMs generativos.

La meta es crear IA que sugiera ideas y construya pruebas verificadas. Los sistemas formales garantizan fiabilidad absoluta. Esto transforma herramientas actuales en colaboradores matemáticos confiables.