ATLAS es una biblioteca masiva de matemáticas formalizadas, desarrollada por Facebook Research, que traduce libros de texto universitarios y de posgrado a código formal utilizando modelos de lenguaje grande (LLMs). Su importancia radica en acelerar el proceso de verificación matemática, permitiendo que conceptos abstractos sean traducidos a un lenguaje computacional estricto, como Lean 4, facilitando la automatización de pruebas y la verificación de resultados.
Funciona mediante un pipeline automatizado llamado AutoformBot, que toma declaraciones informales de áreas como el álgebra, la topología, la geometría diferencial y las ecuaciones en derivadas parciales (PDEs), y las convierte en código Lean válido. El proyecto no solo genera código, sino que incluye métricas de evaluación (como la fidelidad y la integridad de la prueba) para asegurar que la traducción sea precisa. Además, ofrece una herramienta visual para comparar el texto original con su formalización y extraer bloques de código reutilizables.
Este recurso es vital para matemáticos, programadores y científicos de datos interesados en la verificación formal y la inteligencia artificial. Sirve como base para entrenar modelos que realicen matemáticas por sí mismos y proporciona “bloques de construcción” que los humanos pueden usar para iniciar formalizaciones complejas, evitando reinventar la rueda.
Sin embargo, ATLAS es un esfuerzo en curso y no un producto terminado. El código generado es principalmente por máquinas, por lo que requiere curaduría humana para cumplir con estándares estrictos como los de Mathlib. Aunque actualmente cubre 26 libros con más de 600,000 líneas de código y una tasa de éxito del 92.7% en las pruebas, los usuarios deben tener en cuenta que la calidad puede variar y que la contribución externa es bienvenida para mejorar la cobertura y la mantenibilidad.