Proof Assistants

The Curry–Howard correspondence—propositions as types, proofs as programs—offers a conceptual framework for understanding what's missing in current LLMs and what becomes possible when AI systems learn to construct and verify proofs natively.