一句话：在同伦类型论中发展高阶群与连接谱理论，并证明稳定化定理，多数结果在 Lean 中形式化。
本文在同伦类型论中系统发展高阶群理论，涵盖无穷群与连接谱。作者将无穷群视为带基点连通类型中的环路空间，其群结构来自 Martin-Löf 类型论同一类型的固有结构，并由此重新考察普通群、高维群以及可多次去环路（deloop）的群。核心结果是稳定化定理：若一个 n-类型可去环路 n+2 次，则它是无穷环路类型。文章还讨论了这些构造与谱的关系，并且大部分结果已在 Lean 证明助手中形式化。
We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an n-type can be delooped n + 2 times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.