Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Administered by:

Server stats:

3K
active users

mathstodon.xyz: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

Anders Mörtberg

We have now uploaded the final version corresponding to our LICS'23 paper "Formalizing π4(S3)≅Z/2Z and computing a Brunerie number in Cubical Agda" on the arxiv: arxiv.org/abs/2302.00151

Abstract: 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 Z/2Z. 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 normalized to ±2. The question of whether Brunerie’s proof could be formalized in a proof assistant, either by computing this number or by formalizing the pen-and-paper proof, has since remained open. In this paper, we present a complete formalization 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 formalization of a new and much simpler proof that β is ±2. This formalization provides us with a sequence of simpler Brunerie numbers, one of which normalizes very quickly to −2 in Cubical Agda, resulting in a fully formalized computer-assisted proof that π4(S3)≅Z/2Z.

This paper is the result of a lot hard work and countless failed attempts to compute the Brunerie number.

1/3

arXiv.orgFormalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical AgdaBrunerie'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 $\mathbb{Z}/2\mathbb{Z}$. 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 $\pm 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 $\pm 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(\mathbb{S}^3) \cong \mathbb{Z}/2\mathbb{Z}$.
Nov 09, 2023, 08:19 AM·Public·Web
17boosts·20favorites
Public *
Anders Mörtberg

I've given various talks about this, most recently at the HoTT 2023 conferece (staff.math.su.se/anders.mortbe), which I include the following (probably incomplete) timeline of failed attempts to compute this number:

2013: Guillaume presents informal definition of the Brunerie number at an IAS seminar and state the conjecture (see ias.edu/video/univalent/1213/0 at 1:39:50)

December 2014: Guillaume visits Chalmers and tries to compute it with Thierry Coquand and Simon Huber using cubical (github.com/mortberg/cubical)

Spring 2015: I join forces with them and spend a lot of time trying to benchmark and optimize the Haskell implementation of cubical

2016: Guillaume finishes thesis with definition in Appendix B (based on cubical code)

Spring/summer 2017: I port the proof to cubicaltt (github.com/mortberg/cubicaltt/), but computation runs out of memory (on Inria server with 64GB RAM)

June 2017: another attempt in cubicaltt with the MRC group in Snowbird (Vikraman Choudhury, Paul Gustafson, Dan Licata, Ian Orton, and @jonmsterling Optimizes the definition of the number, without luck

Late 2017: I visit Guillaume repeatedly at the IAS and simplify the definition a lot, computation goes slightly further but still runs out of memory

2018: various attempts to run parts of the computation in various cartesian cubical systems (yacctt and redtt) as well as in Cubical Agda, no luck

June 2018: @favonia tries running the cubicaltt computation on a super computer with 1TB of ram, computation stopped after ∼ 90 hours(?)

2/3

Public *
Anders Mörtberg

Summer 2018: Dagstuhl meeting where the cubical group (@jonmsterling, Carlo Angiuli, @favonia , Dan Licata, Simon Huber, Ian Orton, Guillaume Brunerie) found various new optimizations to cubical evaluation (“Dagstuhl lemma”), did not help with computation

2019: @ecavallo ports the definition to Cubical Agda, still running out of memory despite more optimizations (including Cubical Agda “ghcomp” trick of Andrea Vezzosi)

2020-2021: No progress. I was convinced that the only way to make progress was to improve closed term evaluation for cubical type theories...

2022: Breakthrough with Axel Ljungström... A variation on the Brunerie number normalizes to −2 in just a few seconds in Cubical Agda!

The trick to compute -2 relied on a simplified version of the number coming from an ingenious proof of Axel (see the paper), but it still remains open whether Brunerie's orginal definition could actually be computed. I find this on its own a less interesting problem now that we know that we can get the number to compute by first doing some math, but I would still love to have a computational implementation of HoTT where it computes fast as this will surely require making many other things much faster. To this end @AndrasKovacs has been working on an implementation of cubical type theory which takes closed term evaluation seriously called cctt (github.com/AndrasKovacs/cctt). This system has managed to compute various more complicated versions of the number which Cubical Agda has not succeeded in computing, some from the paper with Axel and some by Tom Jack (hott.github.io/HoTT-2023/abstr). However, the original definition still seems out of reach at the moment...

3/3

GitHubGitHub - AndrasKovacs/cctt: high-performance cubical evaluationhigh-performance cubical evaluation. Contribute to AndrasKovacs/cctt development by creating an account on GitHub.
SearchLive feeds
About