Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] The Brunerie number is -2
@ 2022-05-23 19:30 Anders Mortberg
  2022-05-23 19:38 ` Steve Awodey
  2022-05-23 20:22 ` Nicolai Kraus
  0 siblings, 2 replies; 6+ messages in thread
From: Anders Mortberg @ 2022-05-23 19:30 UTC (permalink / raw)
  To: Homotopy Type Theory; +Cc: Axel Ljungström

[-- Attachment #1: Type: text/plain, Size: 2037 bytes --]

We're very happy to announce that we have finally managed to compute the
Brunerie number using Cubical Agda... and the result is -2!

https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S3/Summary.agda#L129

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:

https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S3/DirectProof.agda

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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgLaC1%3DNZYFQdocCjUamCUDJUwGu179XXw%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 2928 bytes --]

^ permalink raw reply	[flat|nested] 6+ messages in thread

end of thread, other threads:[~2022-05-24  9:49 UTC | newest]

Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-23 19:30 [HoTT] The Brunerie number is -2 Anders Mortberg
2022-05-23 19:38 ` Steve Awodey
2022-05-23 20:22 ` Nicolai Kraus
2022-05-23 20:59   ` Anders Mortberg
2022-05-24  9:46     ` Anders Mörtberg
2022-05-24  9:49       ` Anders Mörtberg

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).