From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 11822 invoked from network); 23 May 2022 20:23:14 -0000 Received: from mail-ua1-x93b.google.com (2607:f8b0:4864:20::93b) by inbox.vuxu.org with ESMTPUTF8; 23 May 2022 20:23:14 -0000 Received: by mail-ua1-x93b.google.com with SMTP id k22-20020ab05396000000b00368da315dc1sf4597213uaa.1 for ; Mon, 23 May 2022 13:23:14 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1653337392; cv=pass; d=google.com; s=arc-20160816; b=j6SJ5StODutLwTL4rC8beYHR+9jXgGA+cVDy2RvB6vVMT+DiQM7wVS+2at4BgzJXz7 AK1/Hxe6ZVO+E9g0/KOY/MhTCKGbz50njpo+mf41P8XT6NG7mo6KOaS1XLzsxi16RKdH ADq5JlAbTE9hP6ILQtYlQ346Q+RZViT9aNB/AKVuDXFBw8XtR+aCRQ5rCvplnd2qId7K TBtblN5Awz2NBvaYPtYJnJPc31J25DISu79zsaE7Uf4vkVocMd4BiUZTdq3YnbxbFgW9 wGYO1/cvxyUTdip7aIYVfR83r/YJRxZDqQ8Y9oYLoP2GePm6QjTIKDdjM9/1iDERSO5c ERBg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=QSa3mTuMXCu8GdEHlael/hPPlh2dCkcecH59l0bALP4=; b=L69g+zbggUL1uwZSSUuRs3lj6Mx5dh9Rpx98CUv70jiYGAJE0fZlHu3EP0OGvXfiBx E8ZGeHIuOJi8y9sY1j/2BUg1F5xTu4Ap97nvsH6ViN1+hV0UAENRTdwa98K9A1Aa+KNT LjxYmTitO0TIEi61spMgKf4b+lzUgUSWerI2VPUZOG20HA1amCeGEGb4sOMs7Wqx2MIy Ko85pl44jZOJQCLut0OZyLVpWQeF9ehxMPCLH1MwnqKAohqpnEwQE+4KUTMDcjrslpOC r+X9pw14frt2gsDqL73B1zzd1oEkN1L3hpZpx94KXK7y23nRwxMLUQGubRGYvmPWWsvF MwQA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=EOS10xQW; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2001:4860:4864:20::2e as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-subscribe:list-unsubscribe; bh=QSa3mTuMXCu8GdEHlael/hPPlh2dCkcecH59l0bALP4=; b=fu0GNHAbH+h9LGFVtfJpIyUlbr+UMwaYTxtd1fzdhjF7m8rS/zNJJKxw8vPUzJeqbX W/aZwIWy07X+KfDDo4amGZOsT153TQlJrOEVp7BilTFatJeX8Hx0CZfJQ0Xt9xTWAGvW OL0YmX+gXqOjH/uRwkY/8y35PDd2QeRBFMJXMutOHAHmHetCR/32E13fSNJeJMxpoGAe KIS5h6lj8e1Q8zcE+cTmhV0GMeEGHS/SsfGCu2oVpYIDJornlWSMkeVR570v83+dbEW/ 5ul7wsN4NNNV0xsKGAcSZD11i4GFojfc6dC7cpXhfs5BiJTfQ1G6j2MxVlpsFw/ozKjr DRAQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-subscribe:list-unsubscribe; bh=QSa3mTuMXCu8GdEHlael/hPPlh2dCkcecH59l0bALP4=; b=RI1t0EejGd2inJ50WEHhCPKzRFL7iasWISPiZJfc6eJ5e9z1xy+SSTw6tfLgqOR80E 4ap+KNrJijS6Fc9qB/dOhZblmqF7B2UIQ88/HRw9MC25n4v8jj4VFXnYtpvbvlETrfTl 5auEjt9wYfiIT9yVqHNu4/tN4GgaeYIJBJe4yyS1GZF+h6UrYb3LOUgJ9VCzetc/ebXF QlpyjsIslI1KHSkbHjGy5QpcXWFUUxAmgjyswiHAZjdMoJwzt7E3EuQbQelA6gObRSRu svHP2Cr2Ztm6FCCgNUQ9dwzbfakIrJULIQscP71HoATK0gWAn4aTEh4WmjUw67EL8ZR1 4CnQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-subscribe:list-unsubscribe; bh=QSa3mTuMXCu8GdEHlael/hPPlh2dCkcecH59l0bALP4=; b=lx1HF6IYU1Mh79AFnuPx9P/UUt3Ntq7173qSjDhRzuUPOcguPAJh194nbdiZ9aGSU+ 6mhkn8Hsn8LvxfXTIUXnAcFWJ/QrhePv/FKecMBjSQx95/lRvsK6qB6qyaLrCDJhTKB9 e67Qx/fjyhx7TDvkD9ItJEcMPWXLW2/eMn4AM/CCxU+Ie4FgbC5N5GDpcYFzsz4V27u5 YWnJrmj3xIh2B/iJbYTpnGcVPsrIVk/fioCC70YiOT8Vva3Zvms05gLdxfBAZMTI/+/U Gx8EZ4uU7B9/KS+VZhrKok5eyFYrZJGBzFcGMIXuPCIrvpOEHHxlTPoctA2P9Zu/PfIZ f8ug== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533r58AKiVATzobMA30QpvpTrUHhpotlnwWkOO0EMsnQpoFsJvtp CgFN8CgKNh9WU/7qy/yBNOc= X-Google-Smtp-Source: ABdhPJxRG5y5BeZbKHsL7GuJHK9ArZEAM1EVwBI0YcvUeeJWj2F15D+lhalC+6QMOl0XWXD1j0Tnig== X-Received: by 2002:ab0:2695:0:b0:352:5fc9:4132 with SMTP id t21-20020ab02695000000b003525fc94132mr7861481uao.29.1653337392181; Mon, 23 May 2022 13:23:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6130:3a1:b0:368:dc2b:ead4 with SMTP id az33-20020a05613003a100b00368dc2bead4ls716905uab.8.gmail; Mon, 23 May 2022 13:23:11 -0700 (PDT) X-Received: by 2002:a9f:3193:0:b0:35d:21ec:4ae1 with SMTP id v19-20020a9f3193000000b0035d21ec4ae1mr7778394uad.100.1653337391004; Mon, 23 May 2022 13:23:11 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1653337391; cv=none; d=google.com; s=arc-20160816; b=M0CQ3qO5+UZTeGWrQpczIbJG/ob8a/u9+D6vhnx2NCU7ZzWoOdtbmbLN11e30l9v4O q9JF8H/FeXTGlntSF1zXvXHYSUro1J4U1lA4v18ZseOouFFdzoDBJiVzTeb5WSMQJwzy 3kVHDiOPRufHzz05Mv5y0+n5Efa1pKwbvkjSlWriHznQd9sp6lBuEqt/sYEFJz3wmVY6 32GlfJ0C7IvymvEuH9rZN89CQMmzdWbCA7/cyrLVAcPo3tLLcNqNbkJPeJYYc6N/VR+c HWFJ2TRmAo4VnYMn5DUynrikLDUZr3jOfZSmaQGu/zvgSn4Q81XyRIkgNcd4VzgPGE9Y AjAg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=CT/VwM2+OQTRBNAhJWH3HBQWOwB7sNkS2HQNSENsgnU=; b=Rivvw22FECT6GLwUckUec+ww1l2fInGxmq70zKpbpan9srBbtV9zDftNsss+D3glMM YGHSaSgvSSfBKAiZhaY/8EApvCkwhpVXZUewIb61azNzb9MoxtaEA+RZw+t/dpGdpncs DjL5qNjW0C5tE38wqDNEgq6uForZ702Yvaawaexou1VcsxNAvtyPSN8uYnOnNHtUay5n CtuoDKv+EymjXDCgFU7cn36iQKQMYx2kNU1HVn8Xyf9WMmQEzswFX1/KxW1Cc+Z47Yau xmf7iYpvcrzhepM26jtJZU1tS4UzklhnAVmtBWXtUGV3MKYN+vk+o0iukX7vTIWQh9rB HvWg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=EOS10xQW; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2001:4860:4864:20::2e as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-oa1-x2e.google.com (mail-oa1-x2e.google.com. [2001:4860:4864:20::2e]) by gmr-mx.google.com with ESMTPS id b8-20020ab06e88000000b0035fc4b18c67si1618023uav.2.2022.05.23.13.23.10 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 23 May 2022 13:23:10 -0700 (PDT) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2001:4860:4864:20::2e as permitted sender) client-ip=2001:4860:4864:20::2e; Received: by mail-oa1-x2e.google.com with SMTP id 586e51a60fabf-f16a3e0529so19898228fac.2 for ; Mon, 23 May 2022 13:23:10 -0700 (PDT) X-Received: by 2002:a05:6870:d284:b0:f1:a633:201b with SMTP id d4-20020a056870d28400b000f1a633201bmr459970oae.205.1653337390400; Mon, 23 May 2022 13:23:10 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Nicolai Kraus Date: Mon, 23 May 2022 21:22:59 +0100 Message-ID: Subject: Re: [HoTT] The Brunerie number is -2 To: Anders Mortberg Cc: Homotopy Type Theory , =?UTF-8?Q?Axel_Ljungstr=C3=B6m?= Content-Type: multipart/alternative; boundary="000000000000d948b005dfb39b62" X-Original-Sender: nicolai.kraus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=EOS10xQW; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2001:4860:4864:20::2e as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , --000000000000d948b005dfb39b62 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 =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, 2022 at 8:30 PM Anders Mortberg 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) =3D Z/2Z by Axel Ljungstr=C3=B6m. This new proof involves a ser= ies of > new Brunerie numbers (i.e. numbers n : Z such that pi_4(S^3) =3D Z/nZ) an= d we > got the one called =CE=B2' in the file above to reduce to -2 in just a fe= w > 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'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 th= e > 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 =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 > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgL= aC1%3DNZYFQdocCjUamCUDJUwGu179XXw%40mail.gmail.com > > . > --=20 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 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. --000000000000d948b005dfb39b62 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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--