I did some digging and found the first commit with an attempt to compu=
te the number written by Guillaume Brunerie, Thierry Coquand and Simon Hube=
r 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 a=
lready 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 prob=
lems we had encountered:

https://guillaumebrun=
erie.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 "ghc=
omp" trick which I learned about from Angiuli-Favonia-Harper and which elim=
inates empty systems in hcomps). Now that we have a computation that actual=
ly 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=C3=B6rtberg wrote:

Thanks Nicolai! And yes, our =CE=B2' is a different definition of the or= der of pi_4(S^3). In fact, the number =CE=B2 in the Summary file is not exa= ctly the same number as in Guillaume's Appendix B either for various reason= s. For instance, Guillaume only uses 1-HITs while we are quite liberal in u= sing higher HITs as they are not much harder to work with in Cubical Agda t= han 1-HITs. Also Guillaume of course defines everything with path-induction= while we use cubical primitives and the maps in appendix B are quite unnec= essarily complex from a cubical point of view (for instance, the equivalenc= e S^3 =3D 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 equivalenc= es to define it). One could of course define t= he number exactly like Guillaume does and try to compute it, but I don't fi= nd that very interesting now that we have a much simpler definition which i= s 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 r= oom to make cubical evaluation faster. Surprisingly enough though, one does= n'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:<=
br>

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 p= asses the test that Guillaume formulates in Appendix B of his thesis, right= ? Because this test refers to the Brunerie number =CE=B2 (in the Summary.ag= da file you linked), and not to =CE=B2'.In any case, that's a fa= ntastic result!Best,NicolaiOn 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=20 compute the Brunerie number using Cubical Agda... and the result is -2!The computation was made possible by a new direct synthetic proof that=20 pi_4(S^3) =3D Z/2Z by Axel Ljungstr=C3=B6m. This new proof involves a seri= es=20 of new Brunerie=20 numbers (i.e. numbers n : Z such that pi_4(S^3) =3D Z/nZ) and we got the= =20 one called =CE=B2' 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) =3D = Z / =CE=B2' Z, leading to a proof by normalization of the numb= er as conjectured in Brunerie's thesis.Axel's new proof is very direct and completely=20 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=20 on any special features of cubical type theory=20 and should be possible to formalize also in systems based on Book HoTT.=20 For a proof sketch as well as the formalization of the new proof in just=20 ~700 lines (not counting what is needed from chapters 1-3) see:<= div>=So to summarize we now have both a new direct HoTT proof, not relying on=20 cubical computations, as well as a cubical proof by computation.<= div>Univalent regards,A= nders and AxelPS: the minus sign is a= ctually not very significant and we can get +2 by slightly modifying <= span>=CE=B2', 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 e= mail to HomotopyTypeTh= e...@googlegroups.com.

To view this discussion on the web visit https://groups.google.c= om/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgLaC1%3DNZYFQdocCjUamCUDJUw= Gu179XXw%40mail.gmail.com.

You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.

To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.

To view this discussion on the web visit https://groups.google.c= om/d/msgid/HomotopyTypeTheory/36c1e828-af3a-49c2-840b-1fae9897eeban%40googl= egroups.com.

------=_Part_513_812432203.1653385595287-- ------=_Part_512_343870225.1653385595287--