En 1931, Kurt Gödel demostró que en cualquier sistema formal consistente lo bastante expresivo para la aritmética existen enunciados verdaderos que no son demostrables dentro del sistema. El segundo teorema apunta a la imposibilidad de probar la consistencia del sistema desde dentro.
El golpe al programa de Hilbert redefinió la filosofía de las matemáticas y, más tarde, los debates sobre si “pensar” es solo derivar teoremas. La IA simbólica heredó tanto el poder de los sistemas formales como la conciencia de sus límites.
En 2020–2026, cuando modelos de IA participan en demostraciones asistidas (Lean, Isabelle), el eco gödeliano sigue presente: formalizar no es lo mismo que agotar la verdad matemática.
