Formal Verification of Mathematics in HoTT-Lean
Abstract
This proposal is to support the research group in Formalization of Mathematics in the HomotopyType Theory system implemented in the Lean proof assistant at Carnegie Mellon University.This research group consists of Professors Steve Awodey and Jeremy Avigad and theirgraduate students, in collaboration with other researchers in Computer Science. This group ofexpert researchers are pursuing a recent breakthrough that is reshaping the foundations of inlogic, mathematics, and computer science. Using this breakthrough, new computer systems arebeing developed for the formal verification of mathematical theorems and critical computersoftware. The group at Carnegie Mellon University includes several faculty members, as well aspostdocs and a senior researcher and several graduate students.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jul 28, 2017
- Source ID
- FA95501710260
Entities
People
- Steve Awodey
Organizations
- Air Force Office of Scientific Research
- Massachusetts Institute of Technology
- United States Air Force