I think it goes back to Pontryagin from the late 1930s, though with a rather different argument. The history is a bit confusing because Pontryagin famously made a mistake in computing \pi_4(S^2). But his calculation of \pi_4(S^3) was fine. See Theorem 2' and 2'' of https://people.math.rochester.edu/faculty/doug/otherpapers/pont2.pdf which I found at this webpage that has more history: https://people.math.rochester.edu/faculty/doug/AKpapers.html#2-stem Best, Noah On Tue, Feb 8, 2022 at 10:09 PM Steve Awodey wrote: > Someone please correct me if I am wrong, > but I believe that this was originally proved by J-P Serre in his 1951 > dissertation (using spectral sequences). > So we are about 70 years behind - but catching up fast! > > Congratulations to all who contributed to this milestone! > > Univalent regards, > > Steve > > > On Feb 8, 2022, at 6:24 PM, Joyal, André wrote: > > Dear Anders, > > Congratulation to you and Axel for doing this! > It was a problem for many years! > We can now honestly say that cubical Agda is a serious tool in homotopy > theory! > It is an amazing piece of work. > Thanks to all, starting with Guillaume. > > Best wishes, > Andre > ------------------------------ > *De :* homotopytypetheory@googlegroups.com < > homotopytypetheory@googlegroups.com> de la part de Anders Mortberg < > andersmortberg@gmail.com> > *Envoyé :* 8 février 2022 15:19 > *À :* Homotopy Type Theory > *Objet :* [HoTT] Formalization of π₄(S³)≅ℤ/2ℤ in Cubical Agda completed > > We are happy to announce that we have finished a formalization of > π₄(S³)≅ℤ/2ℤ in Cubical Agda. Most of the code has been written by my PhD > student Axel Ljungström and the proof largely follows Guillaume Brunerie's > PhD thesis. For details and a summary see: > > > https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S3/Summary.agda > > The proof involves a lot of synthetic homotopy theory: LES of homotopy > groups, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey, > Z-cohomology (with graded commutative ring structure), Gysin sequence, the > Hopf invariant, Whitehead product... Most of this was written by Axel under > my supervision, but some results are due to other contributors to the > library, in particular Loïc Pujet (3x3 lemma for pushouts, total space of > Hopf fibration), KANG Rongji (Blakers-Massey), Evan Cavallo (Freudenthal > and lots of clever cubical tricks). > > Our proof also deviates from the one in Guillaume's thesis in two major > ways: > > 1. We found a direct encode-decode proof of a special case of corollary > 3.2.3 and proposition 3.2.11 which is needed for π₄(S³). This allows us to > completely avoid the use of the James construction of Section 3 in the > thesis (shortening the pen-and-paper proof by ~15 pages), but the price we > pay is a less general final result. > > 2. With Guillaume we have developed a new approach to Z-cohomology in > HoTT, in particular to the cup product and cohomology ring (see > https://drops.dagstuhl.de/opus/volltexte/2022/15731/). This allows us to > give fairly direct construction of the graded commutative ring H*(X;Z), > completely avoiding the smash product which has proved very hard to work > with formally (and also informally on pen-and-paper as can be seen by the > remark in Guillaume's thesis on page 90 just above prop. 4.1.2). This > simplification allows us to skip Section 4 of the thesis as well, > shortening the pen-and-paper proof by another ~15 pages. This then leads to > various further simplifications in Section 5 (Cohomology) and 6 (Gysin > sequence). > > With these mathematical simplifications the proof got a lot more > formalization friendly, allowing us to establish an equivalence of groups > by a mix of formal proof and computer computations. In particular, Cubical > Agda makes it possible to discharge several small steps in the proof > involving univalence and HITs purely by computation. This even reduces some > gnarly path algebra in the Book HoTT pen-and-paper proof to "refl". > Regardless of this, we have not been able to reduce the whole proof to a > computation as originally conjectured by Guillaume. However, if someone > would be able to do this and compute that the Brunerie number is indeed 2 > purely by computer computation there would still be the question what this > has to do with π₄(S³). Establishing this connection formally would then > most likely involve formalizing (large) parts of what we have managed to do > here. Furthermore, having a lot of general theory formalized will enable us > to prove more results quite easily which would not be possible from just > having a very optimized computation of a specific result. > > Best regards, > Anders and Axel > > -- > 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 toHomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppmb%2BAt_Bwp_2USKH9dAigFGx0GBrcG3XQQaqZmkr-kHog%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/QB1PR01MB29481886234F6ECEB3006C31FD2D9%40QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.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/021D547B-986C-4E18-B4F2-A105376DE6EB%40gmail.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/CAO0tDg5V2dMm71XbqR4dt%2BK2jCZpE-myseR7385H%3DZGbpoWytQ%40mail.gmail.com.