Formalizing higher categories

Cat­e­go­ry the­o­ry is an ab­stract frame­work used to study math­e­mat­i­cal struc­tures and their re­la­tion­ships. It has sig­nif­i­cant­ly in­flu­enced many ar­eas of math­e­mat­ics and the­o­ret­i­cal com­put­er sci­ence, such as ab­stract al­ge­bra and type the­o­ry. How­ev­er, tra­di­tion­al cat­e­go­ry the­o­ry can­not cap­ture the in­tri­ca­cies of all math­e­mat­i­cal do­mains, re­sult­ing in the de­vel­op­ment of a the­o­ry of "high­er cat­e­gories". This ad­vanced the­o­ry has be­come piv­otal in mod­ern re­search ar­eas such as al­ge­bra­ic topol­o­gy and ho­mo­topy type the­o­ry. Un­for­tu­nate­ly, these ad­vance­ments come at a sig­nif­i­cant price, as high­er cat­e­go­ry the­o­ry is no­to­ri­ous­ly tech­ni­cal and sus­cep­ti­ble to er­rors. The for­mal­iza­tion of high­er cat­e­go­ry the­o­ry presents a promis­ing so­lu­tion to ad­dress these chal­lenges. This has re­sult­ed in sev­er­al for­mal­iza­tion ef­forts, lever­ag­ing a va­ri­ety of proof as­sis­tants, in­clud­ing a re­cent project in Lean, com­menced by Emi­ly Riehl: the ∞-Cos­mos project. In this talk, I will ex­plore the mer­its and lim­i­ta­tions of for­mal­iz­ing high­er cat­e­go­ry the­o­ry with­in Lean, share my ex­pe­ri­ence with the ∞-Cos­mos project, and high­light some tech­ni­cal ob­sta­cles that hin­der fur­ther ad­vance­ments. No pri­or knowl­edge of (high­er) cat­e­go­ry the­o­ry will be as­sumed for this talk.