El artículo «Formal verification and AI are reshaping mathematical research» revela una revolución en el campo de las matemáticas. Mientras que históricamente ha sido un ámbito de trabajo individual y manual, hoy evoluciona hacia un enfoque colaborativo y escalable, gracias a la fusión de LLMs y asistentes de prueba formal (como Lean).

El motor de esta transformación es la complementariedad entre ambas herramientas: los LLMs aportan creatividad y eficiencia en la generación de ideas y automatización de procesos, mientras que los asistentes de prueba aseguran la validez de cada paso. Esta alianza supera el desafío del "factor de Bruijn", permitiendo resolver problemas complejos como los planteados por Erdős.

Más allá de las matemáticas, esta metodología se aplica al desarrollo de software crítico, combinando inteligencia artificial y verificación formal para automatizar la generación de pruebas de corrección, haciendo accesible el software de alta fiabilidad a un público más amplio.