*[HoTT] The Brunerie number is -2@ 2022-05-23 19:30 Anders Mortberg2022-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

*Re: [HoTT] The Brunerie number is -22022-05-23 19:30 [HoTT] The Brunerie number is -2 Anders Mortberg@ 2022-05-23 19:38 ` Steve Awodey2022-05-23 20:22 ` Nicolai Kraus 1 sibling, 0 replies; 6+ messages in thread From: Steve Awodey @ 2022-05-23 19:38 UTC (permalink / raw) To: Anders Mortberg;+Cc:Homotopy Type Theory, Axel Ljungström [-- 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 --] ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [HoTT] The Brunerie number is -22022-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 Kraus2022-05-23 20:59 ` Anders Mortberg 1 sibling, 1 reply; 6+ messages in thread From: Nicolai Kraus @ 2022-05-23 20:22 UTC (permalink / raw) To: Anders Mortberg;+Cc:Homotopy Type Theory, Axel Ljungström [-- Attachment #1: Type: text/plain, Size: 3268 bytes --] Congratulations! It's great that this number finally computes in practice and not just in theory, after all these years. :-) And it's impressive how short the new proof is! But this still doesn't mean that Cubical Agda passes the test that Guillaume formulates in Appendix B of his thesis, right? Because this test refers to the Brunerie number β (in the Summary.agda file you linked), and not to β'. In any case, that's a fantastic result! Best, Nicolai On Mon, May 23, 2022 at 8:30 PM 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 > <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgLaC1%3DNZYFQdocCjUamCUDJUwGu179XXw%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CA%2BAZBBohg%3DXFpJTDiVMaUaNU9O3uA_Q8uqSTGgcJmZD4-oKvUA%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 4660 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [HoTT] The Brunerie number is -22022-05-23 20:22 ` Nicolai Kraus@ 2022-05-23 20:59 ` Anders Mortberg2022-05-24 9:46 ` Anders Mörtberg 0 siblings, 1 reply; 6+ messages in thread From: Anders Mortberg @ 2022-05-23 20:59 UTC (permalink / raw) To: Nicolai Kraus;+Cc:Homotopy Type Theory, Axel Ljungström [-- Attachment #1: Type: text/plain, Size: 4712 bytes --] Thanks Nicolai! And yes, our β' is a different definition of the order of pi_4(S^3). In fact, the number β in the Summary file is not exactly the same number as in Guillaume's Appendix B either for various reasons. For instance, Guillaume only uses 1-HITs while we are quite liberal in using higher HITs as they are not much harder to work with in Cubical Agda than 1-HITs. Also Guillaume of course defines everything with path-induction while we use cubical primitives and the maps in appendix B are quite unnecessarily complex from a cubical point of view (for instance, the equivalence S^3 = S^1 * S^1 can be written quite directly in Cubical Agda while in Book HoTT it's a bit more involved and Guillaume uses a chain of equivalences to define it). One could of course define the number exactly like Guillaume does and try to compute it, but I don't find that very interesting now that we have a much simpler definition which is fast to compute. However, we have come up with various other interesting numbers that we can't get Cubical Agda to compute, so there's definitely room to make cubical evaluation faster. Surprisingly enough though, one doesn't need to do this in order to get Cubical Agda to compute the order of pi_4(S^3) :-) -- Anders On Mon, May 23, 2022 at 10:23 PM Nicolai Kraus <nicolai.kraus@gmail.com> wrote: > Congratulations! It's great that this number finally computes in practice > and not just in theory, after all these years. :-) > And it's impressive how short the new proof is! But this still doesn't > mean that Cubical Agda passes the test that Guillaume formulates in > Appendix B of his thesis, right? Because this test refers to the Brunerie > number β (in the Summary.agda file you linked), and not to β'. > In any case, that's a fantastic result! > Best, > Nicolai > > > > > > > > On Mon, May 23, 2022 at 8:30 PM 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 >> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgLaC1%3DNZYFQdocCjUamCUDJUwGu179XXw%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/CAMWCppmqhhiHkpgHPqoSMvdyQUsT%3DhFevG-LJ8FPhtrLpNtdbQ%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 6510 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread

*2022-05-23 20:59 ` Anders MortbergRe: [HoTT] The Brunerie number is -2@ 2022-05-24 9:46 ` Anders Mörtberg2022-05-24 9:49 ` Anders Mörtberg 0 siblings, 1 reply; 6+ messages in thread From: Anders Mörtberg @ 2022-05-24 9:46 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 6222 bytes --] I did some digging and found the first commit with an attempt to compute the number written by Guillaume Brunerie, Thierry Coquand and Simon Huber already in December 2014: https://github.com/simhu/cubical/commit/6e6278c6a626a9034789ab11cdd6bfb0bc8550be This code is written for the predecessor of cubicaltt called "cubical" and Thierry reminded me that it was based on the buggy regularity evaluator which we eventually fixed in cubicaltt. I also think this cubical code is what became Appendix B in Guillaume's thesis (or maybe Guillaume already had a draft at the time, I don't remember). Anyway, Guillaume gave a nice talk in 2017 with an overview of the attempts up to then and the problems we had encountered: https://guillaumebrunerie.github.io/pdf/cubicalexperiments.pdf This was before Cubical Agda was invented and there are some tricks in Cubical Agda that might make a difference compared to cubicaltt (in particular the "ghcomp" trick which I learned about from Angiuli-Favonia-Harper and which eliminates empty systems in hcomps). Now that we have a computation that actually terminates I'm looking forward to seeing if any of these tricks actually were necessary or if it was "just" a matter of simplifying the definition of the number. Best, Anders On Monday, May 23, 2022 at 11:00:17 PM UTC+2 Anders Mörtberg wrote: > Thanks Nicolai! And yes, our β' is a different definition of the order of > pi_4(S^3). In fact, the number β in the Summary file is not exactly the > same number as in Guillaume's Appendix B either for various reasons. For > instance, Guillaume only uses 1-HITs while we are quite liberal in using > higher HITs as they are not much harder to work with in Cubical Agda than > 1-HITs. Also Guillaume of course defines everything with path-induction > while we use cubical primitives and the maps in appendix B are quite > unnecessarily complex from a cubical point of view (for instance, the > equivalence S^3 = S^1 * S^1 can be written quite directly in Cubical Agda > while in Book HoTT it's a bit more involved and Guillaume uses a chain of > equivalences to define it). > > One could of course define the number exactly like Guillaume does and try > to compute it, but I don't find that very interesting now that we have a > much simpler definition which is fast to compute. However, we have come up > with various other interesting numbers that we can't get Cubical Agda to > compute, so there's definitely room to make cubical evaluation faster. > Surprisingly enough though, one doesn't need to do this in order to get > Cubical Agda to compute the order of pi_4(S^3) :-) > > -- > Anders > > > On Mon, May 23, 2022 at 10:23 PM Nicolai Kraus <nicola...@gmail.com> > wrote: > >> Congratulations! It's great that this number finally computes in practice >> and not just in theory, after all these years. :-) >> And it's impressive how short the new proof is! But this still doesn't >> mean that Cubical Agda passes the test that Guillaume formulates in >> Appendix B of his thesis, right? Because this test refers to the Brunerie >> number β (in the Summary.agda file you linked), and not to β'. >> In any case, that's a fantastic result! >> Best, >> Nicolai >> >> >> >> >> >> >> >> On Mon, May 23, 2022 at 8:30 PM Anders Mortberg <andersm...@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 HomotopyTypeThe...@googlegroups.com. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgLaC1%3DNZYFQdocCjUamCUDJUwGu179XXw%40mail.gmail.com >>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgLaC1%3DNZYFQdocCjUamCUDJUwGu179XXw%40mail.gmail.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- 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/36c1e828-af3a-49c2-840b-1fae9897eeban%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 8850 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [HoTT] The Brunerie number is -22022-05-24 9:46 ` Anders Mörtberg@ 2022-05-24 9:49 ` Anders Mörtberg0 siblings, 0 replies; 6+ messages in thread From: Anders Mörtberg @ 2022-05-24 9:49 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 585 bytes --] > > > This was before Cubical Agda was invented > > Oops, I meant to say that this was around the time Andrea Vezzosi was implementing Cubical Agda (which Guillaume mentions in the slides). -- 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/78088eab-9b8e-4dc3-a2cf-91ae4aa3b5cbn%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 1067 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).