We're very happy to announce that we have finally managed to
compute the Brunerie number using Cubical Agda... and the result is -2!
The
computation was made possible by a new direct synthetic proof that
pi_4(S^3) = Z/2Z by Axel Ljungström. This new proof involves a series
of new Brunerie
numbers (i.e. numbers n : Z such that pi_4(S^3) = Z/nZ) and we got the
one called β' in the file above to reduce to -2 in just a few seconds. With some work we then managed to prove that pi_4(S^3) = Z / β' Z, leading to a proof by normalization of the number as conjectured in Brunerie's thesis.
Axel's
new proof is very direct and completely
avoids chapters 4-6 in Brunerie's thesis (so no cohomology theory!), but
it relies on chapters 1-3 to define the number. It also does not rely
on any special features of cubical type theory
and should be possible to formalize also in systems based on Book HoTT.
For
a proof sketch as well as the formalization of the new proof in just
~700 lines (not counting what is needed from chapters 1-3) see:
So
to summarize we now have both a new direct HoTT proof, not relying on
cubical computations, as well as a cubical proof by computation.
Univalent regards,
Anders and Axel
PS: the minus sign is actually not very significant and we can get +2 by slightly modifying β', but it's quite funny that we ended up getting -2 when we finally got a definition which terminates!