# The formal theory of higher categories

> **NSF 01002526DB NSF RESEARCH & RELATED ACTIVIT** · Johns Hopkins University (MD) · $197,643

## Abstract

Computer proof assistants, software programs that verify the logical reasoning of mathematical proofs written in precise formal language, offer an exciting new paradigm for mathematical research, enabling large-scale collaborations and empowering individual researchers to interact with theorems in other subfields that can be found in large open-source libraries of formalized mathematics. Computer proof assistants are likely to become more integral to the working life of mathematicians in the future.  As different proof assistants often implement the rules of different formal systems, mathematicians may even elect to prove certifiably-correct theorems in a non-standard “synthetic” foundation system. The PI will develop three project clusters that involve computer formalization of higher category theory in parallel with theoretical projects necessary to facilitate this work. The formalization projects each have several student collaborators, who are developing their skills with these tools while making significant scientific contributions.

The first project will introduce (∞, 1)-category theory to Lean’s otherwise broad-ranging library Mathlib via the formalism of an ∞-cosmos, developed in prior joint work of the PI. This approach will leverage Mathlib’s existing bicategories library and largely sidestep the apparent difficulty in formalizing proofs that directly deploy the quasi-categories model. A second project also aims to formalize theorems about (∞, 1)-categories, but 

## Key facts

- **NSF award ID:** 2507077
- **Awardee organization:** Johns Hopkins University (MD)
- **SAM.gov UEI:** FTMTDMBR29C7
- **PI:** Emily Riehl
- **Primary program:** 01002526DB NSF RESEARCH & RELATED ACTIVIT
- **All programs:** Harnessing the Data Revolution, Machine Learning Theory
- **Estimated total:** $197,643
- **Funds obligated:** $197,643
- **Transaction type:** Standard Grant
- **Period:** 09/01/2025 → 08/31/2027

## Primary source

NSF Award Search: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2507077

## Citation

> US National Science Foundation, Award 2507077, The formal theory of higher categories. Retrieved via AI Analytics 2026-06-08 from https://api.ai-analytics.org/grant/nsf/2507077. Licensed CC0.

---

*[NSF Awards dataset](/datasets/nsf-awards) · CC0 1.0*