09-07-2026, 08:00 PM
How I Became Interested in Foundations of Mathematics
Author: Vladimir Voevodsky
Lecture: ASC 2014, Nanyang Technological University, Singapore, 25 August 2014
Vladimir Voevodsky explains how his experience with increasingly complicated mathematical proofs led him toward computer-assisted proof verification and new foundations of mathematics. He contrasts problems such as solving a Rubik’s Cube—where a solution can be checked directly—with advanced mathematics, where even a published proof may contain hidden errors. He recounts his proof of the Milnor Conjecture, which took years to turn from the central idea into a complete rigorous argument, and then describes a more troubling example: a 1991 theorem he proved with Mikhail Kapranov concerning $\infty$-groupoids. Carlos Simpson later produced a counterexample, and in 2013 Voevodsky finally recognized that not merely the proof but the theorem itself, with their chosen definition, was false. This episode convinced him that relying solely on human checking becomes increasingly risky as mathematics grows more complicated.
Voevodsky therefore asks whether mathematical proofs could be checked by computers in much the same way that symbolic computation verifies algebraic identities. To accomplish this, both mathematical statements and proofs must be encoded as symbolic objects—a process called formalization—so that software can verify mechanically that a proposed proof genuinely establishes its theorem. He argues that the traditional foundation of mathematics, ZFC set theory, was developed long before computers and was not designed for convenient formalization of modern mathematics. His search for a more suitable foundation led him beginning around 2006 to Univalent Foundations, connecting Martin-Löf type theory, homotopy theory, and foundations. By 2010 he believed a practical system was emerging, and the 2012–13 IAS program helped develop what became Homotopy Type Theory (HoTT).
The broader aim is not simply to eliminate mistakes but to change how mathematicians work. Voevodsky suggests that the increasing complexity of modern mathematics makes researchers spend more time checking proofs and can make them less willing to pursue daring ideas. Reliable formal verification could transfer part of that checking burden to computers, allowing mathematicians to concentrate more on concepts and discovery. Projects such as UniMath, implemented using the Coq proof assistant, represented early steps toward this vision: large libraries in which definitions, theorems, and proofs can be verified mechanically.
Key takeaways
ARTICLE [PDF]
Author: Vladimir Voevodsky
Lecture: ASC 2014, Nanyang Technological University, Singapore, 25 August 2014
Vladimir Voevodsky explains how his experience with increasingly complicated mathematical proofs led him toward computer-assisted proof verification and new foundations of mathematics. He contrasts problems such as solving a Rubik’s Cube—where a solution can be checked directly—with advanced mathematics, where even a published proof may contain hidden errors. He recounts his proof of the Milnor Conjecture, which took years to turn from the central idea into a complete rigorous argument, and then describes a more troubling example: a 1991 theorem he proved with Mikhail Kapranov concerning $\infty$-groupoids. Carlos Simpson later produced a counterexample, and in 2013 Voevodsky finally recognized that not merely the proof but the theorem itself, with their chosen definition, was false. This episode convinced him that relying solely on human checking becomes increasingly risky as mathematics grows more complicated.
Voevodsky therefore asks whether mathematical proofs could be checked by computers in much the same way that symbolic computation verifies algebraic identities. To accomplish this, both mathematical statements and proofs must be encoded as symbolic objects—a process called formalization—so that software can verify mechanically that a proposed proof genuinely establishes its theorem. He argues that the traditional foundation of mathematics, ZFC set theory, was developed long before computers and was not designed for convenient formalization of modern mathematics. His search for a more suitable foundation led him beginning around 2006 to Univalent Foundations, connecting Martin-Löf type theory, homotopy theory, and foundations. By 2010 he believed a practical system was emerging, and the 2012–13 IAS program helped develop what became Homotopy Type Theory (HoTT).
The broader aim is not simply to eliminate mistakes but to change how mathematicians work. Voevodsky suggests that the increasing complexity of modern mathematics makes researchers spend more time checking proofs and can make them less willing to pursue daring ideas. Reliable formal verification could transfer part of that checking burden to computers, allowing mathematicians to concentrate more on concepts and discovery. Projects such as UniMath, implemented using the Coq proof assistant, represented early steps toward this vision: large libraries in which definitions, theorems, and proofs can be verified mechanically.
Key takeaways
- Mathematical proofs can remain wrong for years, even when written by leading mathematicians and published in respected journals.
- Formalization converts statements and proofs into symbolic expressions that a computer can mechanically verify.
- Voevodsky regarded traditional ZFC foundations as poorly adapted to large-scale computer formalization, motivating his development of Univalent Foundations.
- Homotopy Type Theory and UniMath emerged from this program, combining type theory, topology, and proof assistants in an effort to make computer-verified mathematics practical.
ARTICLE [PDF]
┌────────────────────────────────┐
│ KONSTANTINOS MICHAILIDIS │
└────────────────────────────────┘
│ KONSTANTINOS MICHAILIDIS │
└────────────────────────────────┘