From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-lj1-x23b.google.com (mail-lj1-x23b.google.com [IPv6:2a00:1450:4864:20::23b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a4b33f86 for ; Sat, 25 May 2019 10:22:41 +0000 (UTC) Received: by mail-lj1-x23b.google.com with SMTP id z3sf2274738ljk.1 for ; Sat, 25 May 2019 03:22:41 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558779761; cv=pass; d=google.com; s=arc-20160816; b=eV5OHTGSM+OeMNTXHKeOZi6TaPxoDiUqTdMYKnu4zZ62PKrudRZcDecIEdYMkrPzvN q5715f1pBecbfzBJSVNLabbIeflqOF5jBFF00KM6rsN8NaVml+LhoKz/K+j0QiRSCQzZ 1CPZ4GK6ze1ir9AsxuhKUouIE+yNOyZOnh3JgO70ZL3TRM9/40SGpIYnrAJwgwcMQX4U Zc/3Ickr8OZKqxbabEfHyZhvjTU10LhS5R2O78XJ6HOZ329rjFLL576EI2sP8I6rQMAm nd4g5c2whTyBG5j3NpuyYLA9Ld2/DTmMs3wCYbK5jCbxoj4NFAE/7isbWCXJoRBYTHnf EfNw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:references:message-id :content-transfer-encoding:cc:date:in-reply-to:from:subject :mime-version:sender:dkim-signature; bh=SPR2ORIL8deNO3G0UdEBe30aX9Q5tQMdTo/4Az9nNvk=; b=JPp8o7JAr1QMtwMQCMnKjNZBLtSs4CKUgPivYehqlRprqEUFdRihPdHrasuJrDUqXu mx9oCvY1Lug8AZJXBtbFmQwOvBvnt+y6J040C8JdUnDKRD5bwUQl6TdLYNybIYDXfrEE VeCMLaHyx2JsYL8OptuiASUnTwncmHP2eI4Z4tpUbQ9TMjgegTf1M81pEfJPVIVTnrRF QPYtl5PRInDGzYnL3aCcdiTTddgyxd4YRvfeizocibcEugpILrH2s9mNip1oKYMZlmaD NRcXiRgneWCDjCky+7gR3Lj/0AFXfp/QCVeYbYht5nOfiM7mxt16xtDKijEXBG0ZqG6a f2pw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=sUyTX9Rn; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2a00:1450:4864:20::12a as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=SPR2ORIL8deNO3G0UdEBe30aX9Q5tQMdTo/4Az9nNvk=; b=UmWbIK/iH0+G4cFZlvTzPEM8KFZ/GCb0L4ZDsRu42DKTWZGh9K/rUww/pb/h9V4dvY XyIs9gfmsxsa5O2cdX13pXkhSrurKOS+a+dZ53/T/jLMIC7r6W3bclGqUfHCyP1wmu5U HG4mB4c3zaHQVVKILVLneHNLSgMGsXxY5gWLd+3HQi65F6e+QhKNqZgEQdyJLNBLCh0I nfS4S+2Jx9CwwZaFz29CZ16wUmyB5XfYUesEVctwCp9KlkLEXzDPAXVxAzdr+0FHAf4J BP9tFaLaqA1aZkNbx+5qgiai0yIMRBFnIZYNNww7LIdbYu+uC4gCL0zc6xIeDtiogZjJ HDDg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:subject:from:in-reply-to :date:cc:content-transfer-encoding:message-id:references: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-unsubscribe; bh=SPR2ORIL8deNO3G0UdEBe30aX9Q5tQMdTo/4Az9nNvk=; b=Wn+Gdrkm9bGqqjtpONU0LrxgIDkJr3gRQqC00QP9tgG85QB48MKNpGuuse+6qgO+Ih 4aepMaLcjIjcj2nbOicgZnEvsWdxzjshY/3JmyHfiBIiIOcJD/viOLkbUuJhSV+6e5r+ lsgF6jmPsD6kdPHi92MwbWLLIAYUHlnSKdBb2eB3AjyYwDOBYNuJ5Td/fp8UIEFQEHNl GAuVjzIglDBrjcJkvq0U5LbjAelfBYzFcyGsNw5TMfnfcrpqT8VgsKCn1eeBd3VVj4SL 0Tk4FOcM5WMnqE0XYxp2jQ+xdjm+tF5UbEfnt5LnbJ05ZvFL8Y3zymKG+Expdw42q4rj 0xug== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVqGCwSN5X722i5nFqzSsTkB3Wb7qR2anOctr0OTZyWziHaO4+r bDO0oPuY+qIAmMKkFkJYufU= X-Google-Smtp-Source: APXvYqxo5w1UEkQjg5k8U5TLfR+swEp3QkQKYlAT7MDlrn78hOK3EmROQzlLce1dDriGvNtQTwgTxg== X-Received: by 2002:a19:f506:: with SMTP id j6mr1076896lfb.168.1558779761201; Sat, 25 May 2019 03:22:41 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac2:544a:: with SMTP id d10ls1113661lfn.8.gmail; Sat, 25 May 2019 03:22:40 -0700 (PDT) X-Received: by 2002:ac2:4989:: with SMTP id f9mr54439772lfl.12.1558779760377; Sat, 25 May 2019 03:22:40 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558779760; cv=none; d=google.com; s=arc-20160816; b=rUXhJ08+CW3t1ZvJ2S1A2+e8JMHEEAblhJmROXJhYHRjG/kS+WB8mmpWVWlu4cykmJ KumkwU5QwiWPDEQGvczBBhpAmzWv2OLE3MqSsj8vFtKhqUudqwGhDQEE1NX9whudCLOI HLzrVlYea+LNMlLrgWcE+EMtUbaYFMI8/M4EY6CJAbHbttVFgpuhQf+GAMtf3DloKmGa TwQS2GWMVQqff0Pr9MEwLmYfvi/sWXOmziNxoAcamVdqIVGqar1XVOhyEXeZmiY7I6FD z8az1KkO3JSnZ9iK8c59Jy0kZvl2o7hVvPJ7c3SXCxZI2F4w439Yv9yFuQ7aJsjVoZ4G iGWA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature; bh=2gYLrUBCNnU5m7Zd0c18W1rSaC/+43Di4PkBCgMnc4A=; b=QZ0BAn4oR2CyDOZ1j+VyQRY2VkdRLCiXRUh20Bw2Wnhoq/8KzWe30kYDEHu/XLbs4l 8SdtvIh9QKq0SASIdW35J0eXDxy86Nbt1mHxav7L4mmhNLb7u4oQezU6zllnVpuRJeho u3UUcUyAJhqdht340fl5zdzUptt1dYth2/mPvyfaTgmpPBwb78t6xtTQ2/M/mat663L0 9e59Iex8E8v6NKjj0h+4UXa5ala+3biX8nD65BdBNe4E1JvBTLDascS8KWvmSGrgX1Cc LK4fkuef51sGcSE2IFHhmqFgM0DEXNVzDFHbEVBvah+A0LCiWyvR+dtFqK6iNg+VUamn ojqQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=sUyTX9Rn; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2a00:1450:4864:20::12a as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: from mail-lf1-x12a.google.com (mail-lf1-x12a.google.com. [2a00:1450:4864:20::12a]) by gmr-mx.google.com with ESMTPS id m17si287936ljg.4.2019.05.25.03.22.40 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 25 May 2019 03:22:40 -0700 (PDT) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2a00:1450:4864:20::12a as permitted sender) client-ip=2a00:1450:4864:20::12a; Received: by mail-lf1-x12a.google.com with SMTP id d8so8857461lfb.8 for ; Sat, 25 May 2019 03:22:40 -0700 (PDT) X-Received: by 2002:ac2:593a:: with SMTP id v26mr53150562lfi.64.1558779760156; Sat, 25 May 2019 03:22:40 -0700 (PDT) Received: from [192.168.0.39] (cm-84.208.99.126.getinternet.no. [84.208.99.126]) by smtp.gmail.com with ESMTPSA id x141sm1100380lfd.96.2019.05.25.03.22.38 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 25 May 2019 03:22:38 -0700 (PDT) Content-Type: text/plain; charset="UTF-8" Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.1\)) Subject: Re: [HoTT] doing "all of pure mathematics" in type theory From: Steve Awodey In-Reply-To: Date: Sat, 25 May 2019 12:22:37 +0200 Cc: Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: References: To: Kevin Buzzard X-Mailer: Apple Mail (2.3445.9.1) X-Original-Sender: awodey@cmu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=sUyTX9Rn; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2a00:1450:4864:20::12a as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu 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: , A useful example for you might be Floris van Doorn=E2=80=99s formalization = of=20 the Atiyah-Hirzebruch and Serre spectral sequences for cohomology=20 in HoTT using Lean: https://arxiv.org/abs/1808.10690 Regards, Steve > On May 25, 2019, at 12:12 PM, Kevin Buzzard w= rote: >=20 > Hi from a Lean user.=20 >=20 > As many people here will know, Tom Hales' formal abstracts project https:= //formalabstracts.github.io/ wants to formalise many of the statements of m= odern pure mathematics in Lean. One could ask more generally about a projec= t of formalising many of the statements of modern pure mathematics in an ar= bitrary system, such as HoTT. I know enough about the formalisation process= to know that whatever system one chooses, there will be pain points, becau= se some mathematical ideas fit more readily into some foundational systems = than others. >=20 > I have seen enough of Lean to become convinced that the pain points would= be surmountable in Lean. I have seen enough of Isabelle/HOL to become skep= tical about the idea that it would be suitable for all of modern pure mathe= matics, although it is clearly suitable for some of it; however it seems th= at simple type theory struggles to handle things like tensor products of sh= eaves of modules on a scheme, because sheaves are dependent types and it se= ems that one cannot use Isabelle's typeclass system to handle the rings sho= wing up in a sheaf of rings. >=20 > I have very little experience with HoTT. I have heard that the fact that = "all constructions must be isomorphism-invariant" is both a blessing and a = curse. However I would like to know more details. I am speaking at the Big = Proof conference in Edinburgh this coming Wednesday on the pain points invo= lved with formalising mathematical objects in dependent type theory and dur= ing the preparation of my talk I began to wonder what the analogous picture= was with HoTT. >=20 > Everyone will have a different interpretation of "modern pure mathematics= " so to fix our ideas, let me say that for the purposes of this discussion,= "modern pure mathematics" means the statements of the theorems publishsed = by the Annals of Mathematics over the last few years, so for example I am t= alking about formalising statements of theorems involving L-functions of ab= elian varieties over number fields, Hodge theory, cohomology of algebraic v= arieties, Hecke algebras of symmetric groups, Ricci flow and the like; one = can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Cl= assical logic and the axiom of choice are absolutely essential -- I am only= interested in the hard-core "classical mathematician" stance of the way ma= thematics works, and what it is. >=20 > If this is not the right forum for this question, I would be happily dire= cted to somewhere more suitable. After spending 10 minutes failing to get o= nto ##hott on freenode ("you need to be identified with services") I decide= d it was easier just to ask here. If people want to chat directly I am usua= lly around at https://leanprover.zulipchat.com/ (registration required, ful= l names are usually used, I'll start a HoTT thread in #mathematics). >=20 > Kevin Buzzard >=20 > --=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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.co= m. > For more options, visit https://groups.google.com/d/optout. --=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/BFBE1A09-A246-4DAD-8AD2-25C3C517A7FE%40cmu.edu. For more options, visit https://groups.google.com/d/optout.