In 1931, Kurt Gödel proved that in any consistent formal system expressive enough for arithmetic there exist true statements that are not provable inside the system. The second theorem points to the impossibility of proving the system’s consistency from within.
The blow to Hilbert’s program redefined the philosophy of mathematics and later debates on whether “thinking” is only theorem derivation. Symbolic AI inherited both the power of formal systems and awareness of their limits.
In 2020–2026, as AI models join assisted proving (Lean, Isabelle), the Gödelian echo remains: formalizing is not the same as exhausting mathematical truth.
