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!
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
.