Prospects for Computer Formalization of Infinite-Dimensional Category Theory
summary
Goal is to formalize Joyal–Lurie ∞-category theory; two active efforts use different strategies: Infinity Cosmos in Lean (analytic/axiomatic layer built in mathlib, formalized enriched limits, discovered a faulty con‑complex definition, yet few ∞‑category theorems are finished) and Rzk synthetic HoTT (new type theory where ∞-categories are primitive and several core constructions and a Yoneda‑style lemma are already expressible). Work exposes concrete obstacles: tedious dependent‑type transports, fragile functor/2‑cell encodings, interoperability gaps, and a heavy need for tactics and toolchain support.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 2:30Growing interest in formalization
- 5:40Challenges of infinity category theory
- 17:07Post-rigorous mathematics prospects
- 22:24Three strategies for formalization
- 28:10Lean Infinity Cosmos overview
- 37:21Technical challenges in Lean
- 43:01Synthetic infinity categories in Rzk
- 50:13Future of formalization
- 53:14Q&A
related talks
41mWar Time Proofs and Futuristic Programs
01h 02mTheory and Models of Lambda Calculus Untyped and Typed - Part 4 of 5
33mTheory and Models of Lambda Calculus Untyped and Typed - Part 5 of 5
52mA Categorical View of Adjunctions, Free Constructions, and Profunctor Optics
22mA Certifying Proof Assistant for Synthetic Mathematics in Lean
04mSeparated and Shared Effects in Higher-Order Languages
01h 00mTheory and Models of Lambda Calculus Untyped and Typed - Part 3 of 5
13mTyped Abstractions for Causal Probabilistic Programming