Homotopy type theory and the formalization of mathematics
Abstract
This proposal advances a recent discovery in the foundations of mathematics with far-reaching applications for the modeling of complex systems, the certainty and precision of mathematics, and for the everyday work of mathematicians and other scientists. Homotopy type theory is an emerging field combining logic, mathematics, and computer science and employing a fundamentally new approach based on primitive higher-dimensional structures, and including new principles of reasoning not directly available in conventional foundations. Its applications range from permitting invariant mathematical reasoning with respect to a suitable notion of structural equivalence, to directly expressing higher mathematical concepts such as homotopy types and ¥-categories, to fundamental physics in quantum gauge field theory via an axiomatic extension called cohesion, to providing powerful and flexible computational tools that will facilitate the large-scale formalization of mathematics. Currently, even the most rigorous mathematical proofs are still just arguments in words. Famous examples of erroneous published proofs abound. In principle, proofs are assumed to be reducible to set theory, providing a degree of certainty; but in practice, such reductions are so lengthy and difficult that this foundation is of little practical use in establishing the correctness of mathematical results. Recent advances in high-speed computers have permitted the development of computerized proof systems to aid in the verification of mathematical proofs. In place of set theory these systems typically use constructive type theory, the basic objects of which are structured data types, and which allow the extraction of algorithmic information from the proofs constructed. Unfortunately, such systems are still quite remote from everyday use. The research proposed here, resting on a new homotopical interpretation of such type theories, suggests powerful improvements that allow the effective formalization of wide swaths of mathematics. The technical approaches pursued by this effort are: semantics in ¥-toposes; type-theoretic Quillen model structures; constructive vs. classical foundations; computational implementations; and cohesion in physics. Successful completion of this research may ultimately lead to the widespread use of computational proof assistants in pure and applied mathematics, creating powerful scientific tools with impact on challenging problems of DoD interest.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jun 25, 2021
- Source ID
- W911NF2110121
Entities
People
- Steve Awodey
Organizations
- Army Contracting Command
- Carnegie Mellon University
- United States Army