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