Voevodsky on Inconsistent Mathematics and Univalent Foundations

Recommended as a thought-provoking lecture from a Fields medalist on the foundations of mathematics and formal proof verification.

Vladimir Voevodsky's IAS lecture starts from Godel's second incompleteness theorem to explore whether first-order arithmetic could be inconsistent. It motivates his vision of univalent foundations and computer-checked proofs.