En las últimas semanas se han producido varios avances en la formalización matemática asistida por inteligencia artificial. El 20 de mayo de 2026, ChatGPT refutó la conjetura de la distancia unidad de Erdős en geometría discreta, valiéndose de un profundo teorema de teoría de números de Golod y Shafarevich. Casi de inmediato, la empresa Logical Intelligence, dirigida por el medallista Fields Mike Freedman, logró autoformalizar la demostración completa en el asistente de pruebas Lean.
Un mes después, el 26 de junio, Boris Alexeev, investigador de OpenAI, anunció que había guiado al modelo Sol hasta una formalización completa del contraejemplo, partiendo únicamente de los axiomas de la matemática. En tres semanas, Sol generó 1,2 millones de líneas de código en Lean, una cifra cercana a la mitad de mathlib, la biblioteca matemática de referencia, escrita por humanos a lo largo de nueve años.
El 11 de julio, durante un taller sobre la formalización del Último Teorema de Fermat, el matemático Akhil Mathew comunicó al autor que Sol había hallado un contraejemplo a una conjetura de Grothendieck sobre los esquemas de grupos finitos y libres de orden n. Cuatro horas después, el modelo Fable había autoformalizado las doce páginas del argumento en un archivo de 1.076 líneas de Lean. Estos episodios ilustran un cambio de paradigma: los sistemas de IA ya no solo generan contraejemplos, sino que además los verifican en asistentes de pruebas.