Proof assistants for formalization of higher category theory, dated 23 JUN 2025

The Department of the Air Force Defense Finance and Accounting Service awarded the University of San Diego $958,112 on April 1, 2026 under the Air Force Defense Research Sciences Program (CFDA 12.800) to formalize the theory of weak infinite-dimensional categories using proof assistants.

The award funds development of multiple approaches to formalizing higher category theory, addressing challenges in proving theorems that exist in academic literature as hand-wavy, post-rigorous arguments legible to experts but impenetrable to others. The primary effort, the ∞-cosmos project, aims to axiomatize the category of ∞-categories and formalize central core theory of ∞-categories in Lean's Mathlib for immediate use by mathematicians in other fields. Parallel efforts deploy synthetic foundation systems developed by the principal investigators, including homotopy type theory and univalent foundations, to convert post-rigorous proofs into rigorous arguments in domain-specific foundation systems. Performance occurs in California, with a period of performance from April 1, 2026 through March 31, 2027.

The University of San Diego passes funding to two sub-recipients. Carnegie Mellon University received $250,011 (awarded May 20, 2026) for technology development and student mentoring supporting the formalization work. The Johns Hopkins University received a sub-award (awarded June 8, 2026) also supporting the ∞-cosmos project and synthetic foundation system development.