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 6372 invoked from network); 23 May 2022 19:38:59 -0000 Received: from mail-wm1-x33e.google.com (2a00:1450:4864:20::33e) by inbox.vuxu.org with ESMTPUTF8; 23 May 2022 19:38:59 -0000 Received: by mail-wm1-x33e.google.com with SMTP id l16-20020a05600c1d1000b003974df9b91csf112313wms.8 for ; Mon, 23 May 2022 12:38:59 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1653334738; cv=pass; d=google.com; s=arc-20160816; b=BVa+607udbsMQ5pXfsM7BT84PTtLX/yrjTcQcDlTJzveOJeHQ9DFcm2r0fKHY4w1GB x23fN9oeujVXtNSzUYCqI5bfBvAJv7d8o7zXuUk0ic4GVd1Mo+LdnSlwymCf2Do0w7dd ho6qfv0AOUAFumAt6polLFXnY07MeBXXpE4LZAm6Iaplw4AGRdBkRFlt6lZ4RU/aUs0W Mu9k5OtxrxjHhHbuywWy989ZvJvviH16yDyv+Wj0I3MjWNRBphayblaww1pqoZbq0UjS jXKagJIx2oNm+u3TPSD0XNC9U+0M8cDQ6RxpJBELnRyG0J0WyolBcjEa0Luulpnh2t08 zNnQ== 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:to:in-reply-to:cc:references :message-id:date:subject:mime-version:from:content-transfer-encoding :sender:dkim-signature:dkim-signature; bh=8LZNcwR5mgV1vWCw5ZnsFiskiq4UrStrva7WQLCK1ro=; b=fzhGWzNkn+WMXLM0O2zBtEH0C1XhD2kiTQHM4d07y4+cwLvsyR9LXKTc0CZ2pgoj3c 0cpc0QqjP0QJVEIuIV1Z9+EXIlgNp54bQejk0fSo4LmIqcfC/90xA/acxxJ3UVgZAhNd jv1x1+2P5MPw+IE6qDrUOpxGJtH7I+srbyALvyhkCcMbUcvyQj1vk55MVfmI8RrjoddV wjmSm43x0YNvQo+7bA4Vh02fndkbhv5z7WKcy/PHjCgzwGO6QH/7eNJ4LE0+0RyBft3d M3QsEUhQ6xWFzDTCapQ1ucoUnXbyRggAHmUeaBvj4UpJ6JMf6lVAx7qAZTSd+51PtPW3 fclg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=EVEs9Asd; spf=pass (google.com: domain of steveawodey@gmail.com designates 2a00:1450:4864:20::430 as permitted sender) smtp.mailfrom=steveawodey@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:content-transfer-encoding:from:mime-version:subject:date :message-id:references:cc:in-reply-to:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=8LZNcwR5mgV1vWCw5ZnsFiskiq4UrStrva7WQLCK1ro=; b=YjeV0XBQtGYacAchnD+Dkk0hmblbQKQ43/9+yYRUa17mZRiemBYV+GSCabQug6xAos JoyBNvongubQn7MbwtoAK7oV8nkqesiEE75pVAvD9PFHMCoiUR3aXfCKg3NF1074dpQV EtCsQULNQzI/QzDEgMrCGlu9OsmFsPeLWBG8uTYTdsambauuZ4jbvafsIzTKROjpRpPa C5t78nxwOVgJitN/6G1hllZtcKOvjQURtq3/HqFUjTMgjtezzY6NCG+kya/JH+qvAeFi 9WjySeBqpvHup7316CWdyoFAfSdZtJeKCyubhIqGx8vfgkXJcSYdzLR6qe7pDR+5YMQE SOZA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=content-transfer-encoding:from:mime-version:subject:date:message-id :references:cc:in-reply-to:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=8LZNcwR5mgV1vWCw5ZnsFiskiq4UrStrva7WQLCK1ro=; b=GpR1860TAkV4POn5L6r/txzlHlSxTHUI/hxSMzhq6Whi9iD3/lzV4hxpzdg4M/mkAZ Qi4h2UoksxHqvXRX1FsVt0eSp4JCapitpW8t/UdIg4k3E26a/xRuT9EwFB6qf5PZRWsP 6PP0cPjnLuK8PJvP36fEOzdzPkHBsUsyQyBlISBpqGzLbiI60gVQgdI8MBClC8rQvxBJ 29NgNiPfRNznM9oV/y9KmH2UMDJKgZRSFQs1/J4hdqAxjwugcTeeGZgKs3Eh6sRaN/HP ODWFpPGpbgSM1A3D+f499NQahhKsukSiif842ElFDJdWgs7VprrOKXVe27piU/cjddWH 0P/w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:content-transfer-encoding:from :mime-version:subject:date:message-id:references:cc:in-reply-to:to :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=8LZNcwR5mgV1vWCw5ZnsFiskiq4UrStrva7WQLCK1ro=; b=g6aokivjG/oKCAaE6f5s8YRg4hVkcrnYxaJRnpob4sU7QxRTB7SJQm8+k74HZQrdJ9 TepqtA7k8gstp2EQqr7IwZZh8LhazY+fnwv294PVCxp4NvoVDgz/400bWtVQmHzZm1DV 5UYX2yCu+jFj638amSbzFx2bXFuhANGFPdpEB/mNtuEpfHAVJqwnvzjKOWi+DsYQmqpe la2tdhhjkBe6JLOeUVDaK/Z8J43rQ2Me0AE/Q3lpUrC83u3FYSA9J1NoFK/agbhag0vb 4zUpij49dzbRyslbFAMXpjPO5DIPu9BW/pQnLQaOP87/iNyHSNKeemb9ma9sE+4DSe4r pW7w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532BAHiurxw7rxYE4+ETfqQ5+UrwLw3yDqHrzf5/AcAntZxFrZoW vcLdjShlvhaI3T5KUUppH1A= X-Google-Smtp-Source: ABdhPJyDSzV143dYbr9anI8PeZeZdPYwHcK0ZICGcJSvdi3+L1Z/R1luRl+ZjxjhVJAMrF3zPuWySQ== X-Received: by 2002:a05:600c:1d02:b0:397:5717:5e92 with SMTP id l2-20020a05600c1d0200b0039757175e92mr518307wms.121.1653334738454; Mon, 23 May 2022 12:38:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:4807:0:b0:20f:d148:f68e with SMTP id l7-20020a5d4807000000b0020fd148f68els7598346wrq.3.gmail; Mon, 23 May 2022 12:38:56 -0700 (PDT) X-Received: by 2002:a5d:6d0b:0:b0:20d:681:d301 with SMTP id e11-20020a5d6d0b000000b0020d0681d301mr20075702wrq.364.1653334736776; Mon, 23 May 2022 12:38:56 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1653334736; cv=none; d=google.com; s=arc-20160816; b=ljgf3thiPgaeFSt67dKX0TNopS9yDYvR9KTUemmtyTMOWJ7qgPN+Jp4fD/PCs1C+fw wWu2Tw8/pmaIqIZIaTuLuSXY5rpk82+sT3PB0Z86UcUiR2D4ktAke2t6DibWXe8OB30+ BeHc95sCu3Hy0IB/ndE5COPTO7YevSofmB6whKB4qhU+AXRfuTDWU7+8oZHtJKj6HLsY 6jMG+8ZdiBickn8tSNXEXWrmQ+HQhKLFfi8h7t9eCZ9Kwc6GJbopU+69mxNWIn6g+zv8 LcguCw+VQFYx8lrqMEkKXXc18CXYKd7kXhdvg0MfG/Xlb0AXC6DKHCbnRCpaCKk5Knyu +DiQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:in-reply-to:cc:references:message-id:date:subject:mime-version :from:content-transfer-encoding:dkim-signature; bh=uwXxEb3qLZzJaAiQ0RirvN8GxUJ7X9OKX4lm+VM0Vtc=; b=oxUjFB2pDN5oFTLS3rqKpO4PF6uomWMm4H5rAJrlG3gOj5v0xR9jvHWM1ZlyqMnax8 Qm7neIsUDiDUsEtcpY49PIkaErIlS4rdP+Nlt2jriprRMCCybuWnH/qw7XRej6ld4xc0 CAz058vViYPuYX6Q15kNBDN36RZwxRwXXs5GhwrfHcM9g78miM8mG7BKi6rfjKOlyETj 3xw22OC79YRmNdCReUSAqwPkEQ2WEmLtNBeLauyhNl/yT36GJsDKU6m3v7xH1mzEkHTG HHUY0eyAXf7FQZr6jRR2E8tVG5G1Eq6gFYS5EYjM5rD9wgG2MLZYMcQXmkWLmuKLumZ6 w4yQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=EVEs9Asd; spf=pass (google.com: domain of steveawodey@gmail.com designates 2a00:1450:4864:20::430 as permitted sender) smtp.mailfrom=steveawodey@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wr1-x430.google.com (mail-wr1-x430.google.com. [2a00:1450:4864:20::430]) by gmr-mx.google.com with ESMTPS id bu7-20020a056000078700b0020c9eedfe67si378420wrb.3.2022.05.23.12.38.56 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 23 May 2022 12:38:56 -0700 (PDT) Received-SPF: pass (google.com: domain of steveawodey@gmail.com designates 2a00:1450:4864:20::430 as permitted sender) client-ip=2a00:1450:4864:20::430; Received: by mail-wr1-x430.google.com with SMTP id h5so21662380wrb.11 for ; Mon, 23 May 2022 12:38:56 -0700 (PDT) X-Received: by 2002:adf:e70a:0:b0:20d:e3e:f79f with SMTP id c10-20020adfe70a000000b0020d0e3ef79fmr20472275wrm.105.1653334736279; Mon, 23 May 2022 12:38:56 -0700 (PDT) Received: from smtpclient.apple (2a01cb0404e03a008027ad8d7e6879d0.ipv6.abo.wanadoo.fr. [2a01:cb04:4e0:3a00:8027:ad8d:7e68:79d0]) by smtp.gmail.com with ESMTPSA id y17-20020adfc7d1000000b0020fe43fca50sm3096436wrg.91.2022.05.23.12.38.55 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 23 May 2022 12:38:55 -0700 (PDT) Content-Type: multipart/alternative; boundary=Apple-Mail-A01A7361-32A2-4886-9434-8E5AAE7A58C4 Content-Transfer-Encoding: 7bit From: Steve Awodey Mime-Version: 1.0 (1.0) Subject: Re: [HoTT] The Brunerie number is -2 Date: Mon, 23 May 2022 21:38:55 +0200 Message-Id: <3D8F3A1E-0E9A-47A1-A3B7-CB05B03B802D@gmail.com> References: Cc: Homotopy Type Theory , =?utf-8?Q?Axel_Ljungstr=C3=B6m?= In-Reply-To: To: Anders Mortberg X-Mailer: iPhone Mail (19D52) X-Original-Sender: steveawodey@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=EVEs9Asd; spf=pass (google.com: domain of steveawodey@gmail.com designates 2a00:1450:4864:20::430 as permitted sender) smtp.mailfrom=steveawodey@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: , --Apple-Mail-A01A7361-32A2-4886-9434-8E5AAE7A58C4 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Congratulations to Team A^2! Great work - and a real milestone.=20 Best wishes, Steve=20 > On May 23, 2022, at 21:30, Anders Mortberg wro= te: >=20 > =EF=BB=BF > We're very happy to announce that we have finally managed to compute the = Brunerie number using Cubical Agda... and the result is -2!=20 >=20 > https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S3/= Summary.agda#L129 >=20 > 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 series = of new Brunerie numbers (i.e. numbers n : Z such that pi_4(S^3) =3D Z/nZ) a= nd we got the 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 number as conjectu= red in Brunerie's thesis. >=20 > Axel's new proof is very direct and completely avoids chapters 4-6 in Bru= nerie'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 cubica= l 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:=20 >=20 > https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S3/= DirectProof.agda >=20 > 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. >=20 > Univalent regards, > Anders and Axel >=20 > 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! > --=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= email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgLaC1%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/3D8F3A1E-0E9A-47A1-A3B7-CB05B03B802D%40gmail.com. --Apple-Mail-A01A7361-32A2-4886-9434-8E5AAE7A58C4 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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:
=
=EF=BB=BF=
We're very happy to announce that we have finally man= aged 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 Axel

PS: 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 = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https= ://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgLaC1%3DN= ZYFQdocCjUamCUDJUwGu179XXw%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/msg= id/HomotopyTypeTheory/3D8F3A1E-0E9A-47A1-A3B7-CB05B03B802D%40gmail.com.=
--Apple-Mail-A01A7361-32A2-4886-9434-8E5AAE7A58C4--