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 5309 invoked from network); 23 May 2022 19:30:53 -0000 Received: from mail-pj1-x103c.google.com (2607:f8b0:4864:20::103c) by inbox.vuxu.org with ESMTPUTF8; 23 May 2022 19:30:53 -0000 Received: by mail-pj1-x103c.google.com with SMTP id me18-20020a17090b17d200b001dfa3d25c37sf92218pjb.8 for ; Mon, 23 May 2022 12:30:53 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1653334251; cv=pass; d=google.com; s=arc-20160816; b=U46R6fKu9/ujbWplbGusv2BdkU7fadka0yCXdgI44cOIVyXt45k2df/DKldfVXxRe9 kujMiBXTxTlWo04iwE3ihoPK4eLqxVo6+P5mSdvBnTrluKYNoGVEh3yEMTj4HB8pX4nF 4NeK9dcIvy7bH+s9Fku/f6lj/V2JRfH2Jj2FJZMUZfzzZqlpPmTC6g1AhTIamy9E3509 TEdTTaCwIvRR9LHgu/biavMgUzJBYPfbu9EXcs3HPJVzOUHke+2NbWjFchJpNAmXi4LT fRPTi28QAfoJ7zz5NL7f8RoBJyI9uzEO0qVh0jtByP1mUonBodoSq/oNhuwDNQieqTfL SVYQ== 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 :mime-version:sender:dkim-signature:dkim-signature; bh=8XEvhy1eVyCqWcApOMQVHPEv8Bmman6eek51UUft3dE=; b=EEeIFGLsRjHHlAhOptFQ6K3M87JcOxNso1JOEsNT7iMba+fezToh2ghAmoEYoi3fMH lJDNBYK0KJNiapq8PN9YAJyZGi1Pqn7qzWbx/TUBfRnpxPeMIGkwi6YM5ezsapdUjsr9 DrE4TzlgBb7+sHD8oEpNDJGRA5tA/r1Uw3n+M/jjSmoZoWP3ee5EQTeTUZ4HaAJhjB6+ 3xjig/0b4hfJ5N0pTcge7KMiXU790orNksMi+lXa9oIekaOF+t4hXgPTdza1hEslEmMl tz3bXj2EIaJHiu57f8WsmFL6WigCFslHRXC36d8po3xAHC8FVhkg8Woemr9ClUnf0WVC NaiQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=m9wp2L8j; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::a2f as permitted sender) smtp.mailfrom=andersmortberg@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: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=8XEvhy1eVyCqWcApOMQVHPEv8Bmman6eek51UUft3dE=; b=gBxOe8I3eTCZFvMNvLW6EFkBNfQ8t7Q67WYnX/g8JlpYlPhBKfRcy68WgoVNFqpw9Z L+Gm7VeYfetZ1WTaPye4tlAL/u5MezHKxndKHmyb5X4gxJrAUBypkuaPH0LuCHWaiHk9 ZmE+fe1pqOcYotPsvyzjzTrtMQQOUAYknKQ8Jb+iiCUpQ7vpmrRJyR4LM5Z0VGh6h5Ge qjgI8CyJ1PsyE3BrWmt2yBo28Pr8Bmd01ktfXvtcIdoEFK0yA0G6sXahNRUt6J7W9cqa +RWx6IfsVVtuymoJER5LHIXRAlXtHRMCHCKBUUQMNDOJsyv0FAkWeetRvIjwZ6hnLi1Y ud8g== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version: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=8XEvhy1eVyCqWcApOMQVHPEv8Bmman6eek51UUft3dE=; b=Ydqf1rgnSr22Ifig/yBWIm5x4cvx1Ibh5dBS3KeOC1g4B1K2ZmjOqIUSoxk7ACba3o 7KFxVG21xxDxFpaASkn9GhFKEQ3AEQ5ZUDQwTx6JhN7wqe0FMB1I+Ichb7Wzpw2uGnW4 drr1sdErHg272GuGjvdmPGlUcVvGBCCoQ8QtS4w8uWDHs5M9XrsqIesDzGP2LWNtqnz7 CbDT/qGPTN6rjl01b1PjlNYhrE2fVbPvpOm1tmLOrvof3SLZMY79c3cDEC4b8DMPOWns 72am85oKCEvwp8jTJ9Mu3q28Z+uLQzNiAxdTPNBMvoVM6ufA/s//E20WlbqjnGyZjJ6H ErlA== 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: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=8XEvhy1eVyCqWcApOMQVHPEv8Bmman6eek51UUft3dE=; b=eNcvLjjzb40bIVopD7cZDAFZXh6fAKAHLk+hV3Bt17r//jzsyYLWSjDIYSDJ3yRamv frd2vH8oR8XoBnb8RKQuQDx5mB6jKq3cBvZKAs48ntzjdjAmxWec79McNSuV2UGoYYbl gSdkguHrl60cSlnQDCj0mik1UDK6QwV1hFiYRrnfVgJd8sPxuYGd0g/KXV/yeHZkEct6 V5TpAlf2G25PViywDkcQz5DvUwJrAmad2mDet6aijtxjWWhTSvhAwAWpwbL51uY0SglT VpsKXYTvlklP9dG/3jLFtMPyHU2AlWwu2W+MUnwdv0LZznFqsNyoF4vRjXiER/P/66Rk n0iw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530dY2O+a1Jic77KNw71CxmkYxN/w0QU+sLAqYY//T7MrqXhRiaW W5WzlneoNUnnu699dzKKvSw= X-Google-Smtp-Source: ABdhPJzycAcDg7xFH6ZN0XJ1Eoj1wCJK4Be5YlDaWvXYVAMBnkqNLWBul7tadbBETPVdGywOZnhDYg== X-Received: by 2002:a17:903:40cf:b0:161:6650:e244 with SMTP id t15-20020a17090340cf00b001616650e244mr23655431pld.128.1653334251293; Mon, 23 May 2022 12:30:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:bb8c:b0:14d:d65a:dbdb with SMTP id m12-20020a170902bb8c00b0014dd65adbdbls9301626pls.6.gmail; Mon, 23 May 2022 12:30:49 -0700 (PDT) X-Received: by 2002:a17:902:ed82:b0:158:fef8:b501 with SMTP id e2-20020a170902ed8200b00158fef8b501mr23534703plj.47.1653334249765; Mon, 23 May 2022 12:30:49 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1653334249; cv=none; d=google.com; s=arc-20160816; b=TbGp4QdaJ7SfLoP4kQsBUpKhP0dQKaE2Y9QwjnAuJJXXTSnqEnl0tvYy5DvbPb2yBi vbhY/Q5cEmJnYEtfmpoV4iMCS+e1jH7I7gERzUhwhSUENb4PR5gB6HTyfxkdJ3E47xxv FsmXakVbHpLMeiI/ZSf2hwfnScm/SMGN63MnQpls1CUYhLqRLe9eQWzdXFO+qcUWAMGD SDUhN2V4d792S8DvjNSM1m4ZXiw/d1Nic9waViYmrQBVUulFq1NVVXWDEFWnGFUkX/oN Zu2kdmyS6MZwNke0VLLLw6+b0CAdLAXRQ0RDVdwNKjIjZH06UkxfMs6IKED7MsNptx61 iHUw== 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:mime-version:dkim-signature; bh=45fBVUgX6ufXpd2KkI/NO+KmaTZ94JAkhAbblncpA50=; b=lYOQD6Fwgv96GQJKLU9RmnR4i8bu3C1cggBCfUQ/Ug5gIAxEwsjATZF21huBipL9iS ViVNgeLppeP7NxSUG04L6Kl9Ua++1ODYvl1Hy+jwju5+ZpAfISd4U8IEFNfxf8s29TfO O5ay3p3SMXn0EWd5ss12mkRppEaoGxTSAN9O4e33OTWxXZVU0nGhbKFNHEh+/te18vIR wmHL+hnDDnStifuW7xPOKc8NaXeoPKCoogJLQBAErcAGvYEET7uBCVfBF3JLFtds0tKg tTRoxM8mlebUPXfeOWSX30JoIE8Q0Cnl5dmwMYHiGC5CG+3Rlnl5vUUXj6nq80h2kjXI jOWQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=m9wp2L8j; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::a2f as permitted sender) smtp.mailfrom=andersmortberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vk1-xa2f.google.com (mail-vk1-xa2f.google.com. [2607:f8b0:4864:20::a2f]) by gmr-mx.google.com with ESMTPS id h18-20020a056a00171200b004e1a39c4e87si596092pfc.0.2022.05.23.12.30.49 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 23 May 2022 12:30:49 -0700 (PDT) Received-SPF: pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::a2f as permitted sender) client-ip=2607:f8b0:4864:20::a2f; Received: by mail-vk1-xa2f.google.com with SMTP id d132so7583335vke.0 for ; Mon, 23 May 2022 12:30:49 -0700 (PDT) X-Received: by 2002:a1f:3194:0:b0:34d:5744:245c with SMTP id x142-20020a1f3194000000b0034d5744245cmr8474646vkx.12.1653334249154; Mon, 23 May 2022 12:30:49 -0700 (PDT) MIME-Version: 1.0 From: Anders Mortberg Date: Mon, 23 May 2022 21:30:13 +0200 Message-ID: Subject: [HoTT] The Brunerie number is -2 To: Homotopy Type Theory Cc: =?UTF-8?Q?Axel_Ljungstr=C3=B6m?= Content-Type: multipart/alternative; boundary="0000000000009daf8805dfb2e09b" X-Original-Sender: andersmortberg@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=m9wp2L8j; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::a2f as permitted sender) smtp.mailfrom=andersmortberg@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: , --0000000000009daf8805dfb2e09b Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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/Su= mmary.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 serie= s of new Brunerie numbers (i.e. numbers n : Z such that pi_4(S^3) =3D Z/nZ) and = 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 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 the 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/Di= rectProof.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! --=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/CAMWCppkF0JTQ8z6sPgLaC1%3DNZYFQdocCjUamCUDJUwGu179XXw%40= mail.gmail.com. --0000000000009daf8805dfb2e09b Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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 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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppkF0JTQ8z6sPgLaC1%3DNZYFQ= docCjUamCUDJUwGu179XXw%40mail.gmail.com.
--0000000000009daf8805dfb2e09b--