Formal Verification of Mathematics in HoTT-Lean
Abstract
This proposal supported the research group in Formalization of Mathematics in the Homotopy Type Theory system, implemented in the Lean proof assistant at Carnegie Mellon University. This research group consists of Professors Steve Awodey and Jeremy Avigad and their graduate students, in collaboration with other researchers in Computer Science. This group of expert researchers are pursuing a recent breakthrough that is reshaping the foundations of in logic, mathematics, and computer science. Using this breakthrough, new computer systems are being developed for the formal verification of mathematical theorems and critical computer software. This proposal supported two graduate students and provided summer salary for one faculty member. This support strengthened the CMU research group and enabled a more robust effort. Specific outcomes included two doctoral dissertations, an extensive library of formalized mathematics, and numerous conference and journal publications. The doctoral dissertation of Floris van Doorn developed a module for homotopy type theory within the new Lean proof assistant, which is currently under development at CMU, and formalized a large amount of algebraic topology and homotopy theory therein, including the Serre spectral sequence. The doctoral dissertation of Egbert Rijke investigated synthetic homotopy theory and developed the new notion of an infinite-dimensional equivalence relation, as a step toward solving a longstanding coherence problem in homotopy type theory. In addition to supervising the doctoral students and collaborating on their research, the PI investigated impredicative encodings of higher inductive types, including their realizability semantics.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 14, 2019
- Accession Number
- AD1085819
Entities
People
- Steve Awodey
Organizations
- Carnegie Mellon University