The formal theory of higher categories

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 in a non-standard foundation system designed to make conceptually-simpler constructions and proofs fully rigorous. There is an experimental computer proof assistant Rzk that verifies proofs written in simplicial homotopy type theory, a formal system developed in prior joint work of the PI, and ongoing work to formalize (∞, 1)-category theory in this synthetic framework. This project aims to expand this system, which is insufficiently expressive to encompass the full theory of (∞, 1)-categories, without narrowing its semantics, which include (∞, 1)-categories defined internally to an arbitrary ∞-topos. The final project aspires to develop a prototypical synthetic theory of (∞, n)-categories by developing a new type theory for marked shapes to provide a finitary syntactic encoding of (∞, n)-categorical data with semantics in the new comical spaces model. These pen-and-paper developments will enable (∞, n)-category theory to be formalizable in the future, once a suitable computer proof assistant is built to implement the rules of this new proposed formal system. The medium-term objectives include specific formalization targets that will then be available to other users of Lean’s Mathlib and Rzk’s simplicial homotopy type theory libraries. The long-term objective is to make (∞, 1)-category theory and eventually also (∞, n)-category theory more accessible to non-experts, who could use the computer formalized proofs as ingredients in their work. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.