# * 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.

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.