El artículo «Formalization of Erdős problems» destaca el auge en la resolución de problemas de Paul Erdős gracias a la web erdosproblems.com y el proyecto Formal Conjectures. De más de 1100 problemas recopilados, el 40% ya están resueltos y unos 240 tienen sus enunciados formalizados en Lean. Esta infraestructura comunitaria y el uso de bases de datos han acelerado notablemente el progreso matemático.

La gran revolución descrita es el uso de IA para formalizar y resolver estos retos. Herramientas como Aristotle ya no solo asisten, sino que traducen demostraciones de lenguaje natural a código Lean automáticamente. Incluso han logrado hitos históricos al resolver problemas abiertos (como el problema 124) de forma totalmente autónoma, generando nuevas matemáticas verificadas sin ayuda humana.

Finalmente, el autor advierte sobre la "malformalización": errores sutiles al traducir enunciados a código, desde bugs técnicos hasta la omisión de hipótesis necesarias. A pesar de estos desafíos, concluye que el ritmo de avance es vertiginoso y que la comunidad de Erdős está sirviendo como modelo pionero para integrar la IA en la investigación matemática formal.