Congratulations! It's great that this number finally c=
omputes 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=
9;t mean that Cubical Agda passes the test that Guillaume formulates in App=
endix B of his thesis, right? Because this test refers to the Brunerie numb=
er =CE=B2 (in the Summary.agda file you linked), and not to =CE=B2'.

In any case, that's a fantastic result!

Best,

Nicolai

On Mon, May 23, 20=
22 at 8:30 PM Anders Mortberg <andersmortberg@gmail.com> wrote:

We're very happy to an= nounce 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 ju= st 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 number as conjectured in Brunerie's thesis.Axel&= #39;s new proof is very direct and completely=20 avoids chapters 4-6 in Brunerie's thesis (so no cohomology theory!), bu= t 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 Axel

PS: the minus sign is a=
ctually not very significant and we can get=C2=A0+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 &= 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.com/d/msgid/HomotopyTypeTheory/CAMWCppkF= 0JTQ8z6sPgLaC1%3DNZYFQdocCjUamCUDJUwGu179XXw%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.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBohg%3DXFpJTDiVMaUaNU= 9O3uA_Q8uqSTGgcJmZD4-oKvUA%40mail.gmail.com.

--000000000000d948b005dfb39b62--