Formalising and Computing the Fourth Homotopy Group of the 3-Sphere in Cubical Agda
arxiv(2023)
摘要
Brunerie's 2016 PhD thesis contains the first synthetic proof in Homotopy
Type Theory (HoTT) of the classical result that the fourth homotopy group of
the 3-sphere is ℤ/2ℤ. The proof is one of the most
impressive pieces of synthetic homotopy theory to date and uses a lot of
advanced classical algebraic topology rephrased synthetically. Furthermore, the
proof is fully constructive and the main result can be reduced to the question
of whether a particular "Brunerie number" β can be normalised to ± 2.
The question of whether Brunerie's proof could be formalised in a proof
assistant, either by computing this number or by formalising the pen-and-paper
proof, has since remained open. In this paper, we present a complete
formalisation in Cubical Agda. We do this by modifying Brunerie's proof so that
a key technical result, whose proof Brunerie only sketched in his thesis, can
be avoided. We also present a formalisation of a new and much simpler proof
that β is ± 2. This formalisation provides us with a sequence of
simpler Brunerie numbers, one of which normalises very quickly to -2 in
Cubical Agda, resulting in a fully formalised computer-assisted proof that
π_4(𝕊^3) ≅ℤ/2ℤ.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要