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

~ David Roberts
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!)

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

  2. I’ve never quite understood this story. Am I right in thinking that one can just write down the usual maths proof that pi_4(S^3)=Z/2Z and that would be fine to do in a theorem prover? But somehow these people are trying to prove this theorem in a very specific way, which turns out to involve a gigantic computation (far larger than any computation which is done in the usual proof), and then the issue is that they can’t do this computation because they run out of memory? Have I got this straight?

    Like

    Reply

    1. It’s more like they formalise not this theorem, but merely \exists n:N pi_4(S^3)=Z/nZ. Classically this would be like proving that pi_4(S^3) is a finite group with one generator. And then the code runs the algorithm that proves such a number exists, by actually constructing it as a numeral, namely SS0.

      One could in principle formalise Brunerie’s paper proof of n=2 in a proof assistant that allows univalence, and that is a more prosaic proof more analogous to the usual proof. But the computational challenge is not to formalise this with computational output, but the pure existence statement.

      Like

      Reply

      1. I see! Are there other higher homotopy groups of spheres which one can prove are cyclic using this method? And the point is that if you never assume the law of the excluded middle or the axiom of choice in your proof, every number which shows up in your proof is in theory computable so you can attempt to stare at the proof and evaluate the number.

        I guess one way of interpreting the current state of things is that it demonstrates that this is a lousy way of actually computing pi_4(S^3), in the sense that we could instead formalise the usual proof given in a graduate topology course and it wouldn’t have this problem (although of course it would be some hard work to do this! But it would not run into issues of the inability to do a gigantic calculation). Similarly let’s say we wait until computers are 1000000 times better and then it turns out that we can compute that pi_4(S^3)=Z/2Z with this method. We’re then immediately faced with the problem that we can’t do pi_5(S^3), whereas the classical approach https://en.wikipedia.org/wiki/Homotopy_groups_of_spheres#Table has given us dozens of nontrivial examples of homotopy groups of spheres. I guess the traditional approach is almost certainly not constructive in the sense that it will use the law of the excluded middle somewhere, but I am unclear about whether this constructive approach actually buys you anything from the point of view of, say, a working topologist.

        My take home from this story (hopefully I’ve got my facts straight) is that it (n=2) is a very interesting example of something which can be proved classically, but there is a much longer constructive proof and the challenge is to formalise this constructive proof. And it is a nice “sweet spot” because it’s out of reach right now but one could envisage that with some more good ideas, and as more powerful computers become more accessible, it might become within reach, thus making it a good problem to work on. There is a computational side to the question and also a constructive mathematical side to it, because there could be speed-ups coming from both domains.

        Like

  3. The computational proof isn’t meant to be the best way to compute further homotopy groups in HoTT, but is more of a test of the computational nature of cubical type theory. Traditional methods should work, but there are substantial challenges and new phenomena!

    For example, there are ∞-toposes (models of HoTT) in which the universal coefficient short exact sequence is instead a universal coefficient spectral sequence. And in which Ext^n(A, B) can be non-zero for abelian groups A and B and n > 1. (Work in progress with Jarl Flaten.) And in which a set can have non-trivial higher cohomology. (https://homotopytypetheory.org/2013/07/24/cohomology/)

    When we prove something in HoTT, we are not just proving it for spaces, but for all ∞-toposes, so one expects there to be such twists. This makes it a lot of fun!

    Like

    Reply

    1. I see. You’re stressing the point that this S^3 is not an “analytic” S^3 (i.e. some subset of points in R^4) but a “synthetic” S^3 (an abstract “space” (i.e. some higher inductive type) satisfying some rules) and so the argument works in any situation where those rules are obeyed and can thus be said to be a proof of a more general theorem.

      Like

      Reply

      1. Yes. More precisely, one can form S^0 by taking the disjoint union of the terminal object with itself, and then one can form S^3 by suspending S^0 three times, where the suspension of an object X in an ∞-topos is defined as the pushout of X along two copies of the map to the terminal object. Also in any ∞-topos, one can form the loop space of a pointed object Y as the pullback of Y along two copies of the map from the terminal object that defines the pointing. Finally, in any ∞-topos one can define the 0-truncation as the left adjoint to the inclusion of the 0-truncated objects; this corresponds to π_0, which forms the “set” of components of an object. Combining all of this, one can define π_4(S^3) as the 0-truncation of the fourth loop space of S^3. A proof in HoTT that π_4(S^3) is Z/2 proves that in any ∞-topos π_4(S^3) is equivalent to the (internal) Z/2.

        Here’s an example that might be more interesting to you. At first, it might seem disappointing that we can’t prove in HoTT that Ext^n(A,B) = 0 when n > 1 for abelian group objects A and B. But in sheaf models, A and B correspond to sheaves of abelian groups and these Ext groups turn out to correspond to sheaf Ext, which is something that algebraic geometers already study. So the things we can prove about Ext in HoTT turn out to imply things about sheaf Ext. The extra generality here isn’t just abstract nonsense, but helps in concrete situations. So while one could add axioms to make HoTT behave more like classical mathematics, one would then rule out these models that are important examples that arise in applications.

        Another point to make is that knowing about these models is important for realizing what things you can’t expect to be able to prove in HoTT.

        Like

Leave a reply to xenaproject Cancel reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.