KnowledgeBase » 
PUBLICATION
» ID = 775
Computer Science at the Frontiers of Mathematics
by Robert L. Constable
2020
Increasingly computer science is engaged at the frontiers of mathematics. One recent example is
research in the Computer Science Department at Cornell University in the area of mathematics
called homotopy theory. One of the world’s best mathematicians, the Fields Medalist Vladimir
Voevodsky, working at the Institute for Advanced Study near Princeton University, sought help in
confirming the validity of a proposition he called the Univalence Axiom. One way of confirming
the correctness of proposed axioms is to formalize the theory in which they are stated. That
means formulating all of the definitions and theorems extremely precisely so that every detail of
purported proofs can be checked by a computer using only the primitive notions of the theory
and the axioms of logic.