From: Steve Awodey <steveawodey@gmail.com>
To: Anders Mortberg <andersmortberg@gmail.com>
Cc: "Homotopy Type Theory" <homotopytypetheory@googlegroups.com>,
"Axel Ljungström" <axel.ljungstrom@math.su.se>
Subject: Re: [HoTT] The Brunerie number is -2
Date: Mon, 23 May 2022 21:38:55 +0200 [thread overview]
Message-ID: <3D8F3A1E-0E9A-47A1-A3B7-CB05B03B802D@gmail.com> (raw)
In-Reply-To: <CAMWCppkF0JTQ8z6sPgLaC1=NZYFQdocCjUamCUDJUwGu179XXw@mail.gmail.com>
[-- Attachment #1: Type: text/plain, Size: 2633 bytes --]
Congratulations to Team A^2!
Great work - and a real milestone.
Best wishes,
Steve
> On May 23, 2022, at 21:30, Anders Mortberg <andersmortberg@gmail.com> wrote:
>
>
> 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.
--
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/3D8F3A1E-0E9A-47A1-A3B7-CB05B03B802D%40gmail.com.
[-- Attachment #2: Type: text/html, Size: 4069 bytes --]
next prev parent reply other threads:[~2022-05-23 19:38 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2022-05-23 19:30 Anders Mortberg
2022-05-23 19:38 ` Steve Awodey [this message]
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
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=3D8F3A1E-0E9A-47A1-A3B7-CB05B03B802D@gmail.com \
--to=steveawodey@gmail.com \
--cc=andersmortberg@gmail.com \
--cc=axel.ljungstrom@math.su.se \
--cc=homotopytypetheory@googlegroups.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
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).