Ljungström – theHigherGeometer

Agda code:

-- Second "Brunerie number"
open HⁿℂP² using (g)
brunerie2 : ℤ
brunerie2 = g 1

There is an open problem in computational HoTT/synthetic homotopy theory, namely to get a computer to evaluate the proof in HoTT that there is a natural number $n$ , such that $\pi_4(S^3)\simeq \mathbb{Z}/n\mathbb{Z}$ , and spit out the answer $n=2$ . This number $n$ is known as Brunerie’s number, as the proof that there exists such an $n$ was given by Brunerie, who then gave an on-paper proof in HoTT that it is indeed 2.

The only way to compute Brunerie’s number is to have an implementation of some version of HoTT in which the univalence axiom will actually compute, and so far this means using a proof assistant that uses cubical type theory. The inefficiencies in existing software and/or lack of computing power mean that despite starting a formal proof running that would calculate Brunerie’s number, it hasn’t been achieved.

This means that it would be nice to have a slightly easier problem of the same nature to test out ideas in computational synthetic homotopy theory. Guillaume Brunerie, Axel Ljungström and Anders Mörtberg have supplied just one such problem, in Synthetic Cohomology Theory in Cubical Agda and even implemented in cubical Agda, namely to decide the degree of the cup-square map

$\mathbb{Z} \simeq H^2(\mathbb{CP}^2)\stackrel{x\mapsto x\smile x}{\longrightarrow} H^4(\mathbb{CP}^4)\simeq \mathbb{Z}$

Namely, if $g$ denotes this homomorphism $\mathbb{Z}\to\mathbb{Z}$ , and $e$ is a generator of $H^2(\mathbb{CP}^2)$ , then $g(e)=\pm 1$ . This is proved using on-paper HoTT in Chapter 6 of Brunerie’s thesis, using Gysin sequences, and is rather complicated. Brunerie, Ljungström and Mörtberg say that if one could simply compute $g(e)$ —what they call “a second Brunerie number”—by running the cubical Agda code, then the actual proof that it is $\pm1$ is not needed.

However, the computation still is not efficient enough, or the software design clever enough, for it to actually finish. But the authors write

This computation should be more feasible than the original Brunerie number. As our definition of ⌣ produces very simple terms, most of the work has to occur in the two isomorphisms, and we are optimistic that future optimizations will allow us to perform this computation.

Hence we might actually see this number be calculated. It’s mildly amusing to me that we cannot compute the number 2 (the original Brunerie number) with a TB of RAM and 90 hours of computation, so HoTT-ists propose calculating 1 instead, and we still cannot do it (but might in the future!)

Tag: Ljungström

A new “Brunerie number”, might be easier to calculate?