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.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x23c.google.com (mail-oi1-x23c.google.com [IPv6:2607:f8b0:4864:20::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 46cc0fe5 for ; Sat, 25 May 2019 10:12:07 +0000 (UTC) Received: by mail-oi1-x23c.google.com with SMTP id z1sf4375391oic.11 for ; Sat, 25 May 2019 03:12:06 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=+nsqc5s9SOA0OIfAb2+ngYjQIUrzqm/LUuUFU3+u7as=; b=C8ltUcKeMUno5oSlYnIGvnw+o45UxCOjNR9u7LeDYZl5BppBnGlJvprFjk+4xN7HzP BmxwvUh62/tFm+MadMWDOSRK2ZdTBIR8QimD9OacHHO3gvD4CV7qcQNupIOgCIk4a78M aFrJvrBgEJBt2TLDF5CDhOGtUzrVfKg/iJAgnoAZ1F3KBO5riVuRbdHgbsO6zbgqQqQv ANQloKVDqEXTEaXH2KjuelyyJ6MpuXsmcSfatWRmGfNCbPwRzUKyIm4+Y5wD3Cqbp6gp FkzNVvLH0I3Ptglawsvb+a48ra0O9FlI892ci9hoQB8grkjbxRp0I3T8Vp5kPYXjUP39 ZfzA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=+nsqc5s9SOA0OIfAb2+ngYjQIUrzqm/LUuUFU3+u7as=; b=XJ7t3XMq6axY6o8sJXqyALUC43X0F1ND8ib5VyTKuM5pFLOnXh1s9i69dyX6105JE8 h5nBftSa66FsFDH++1EIfA9b6xQw0XDxAoEH4wlbOYGSNd13exCW+pWIXBVGLrYjNLMc Nz1Q8DgbIVy57PpsDwOgN8w8yPGkD6gAxSpYPqE+M2ABlDN/7QDRiItKrMvbXAQ2GiDM 61+Nuu2X5TPbQJqkT9gxyL85E5DqJN5JVhj3RWqPn3FoecQe6FThn+LXktwooDmV1wso 0aoJFHJmsuJO4uL4RFyR84kLnELKxlS+XAhiC56S0Hel6u8G9Z7i9ovp5QqeZPtcIhcl Y29w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=+nsqc5s9SOA0OIfAb2+ngYjQIUrzqm/LUuUFU3+u7as=; b=HE3BFNf3xW33WHwO64EbQsDOcb+qf6zU0K9mnx4Ctc3h8BpglUcWqyfKyW5+wIjPN1 hmVqGYhf7UnnfpTCIRu31Hg20WZNnq/GxSqvYlIUnbq95DK8xhkqgvAlgqEsem8YfzXb SeXN6mHQbP+qZhNIQxkdvY3iyEDl2fOf1+LJC60egIc+YxlSH2iVlN/xGSbEqlk5/lam ZcFTh5qTbwwoGqVKhHekovkgP3lu9fftcv05AFK63ILSDbCDLUUgS0yILbipN8RWRF7S xCnEaYnBoKeU3fIH5maovf8htebO4CA1c+OJKGTtlorlXniaMsi9LEKEZP6NExvRk9GV 9RCA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUSS9oGNG7gY7gjnL9alECKPBxIBBHlOof+9tyn/Ld6qEEVEtql G0XkTlzCBw4SYxfax/BkhtA= X-Google-Smtp-Source: APXvYqzommZaXM0eEJyGTL+kYYrXoLoW/5tn4UWLyiSgbv7XTth33kiMnXyOj0B+7MjcxqsyVwtm6w== X-Received: by 2002:aca:5c06:: with SMTP id q6mr26776oib.8.1558779125525; Sat, 25 May 2019 03:12:05 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:49cf:: with SMTP id w198ls1819557oia.13.gmail; Sat, 25 May 2019 03:12:05 -0700 (PDT) X-Received: by 2002:a05:6808:28f:: with SMTP id z15mr8605847oic.32.1558779125096; Sat, 25 May 2019 03:12:05 -0700 (PDT) Date: Sat, 25 May 2019 03:12:04 -0700 (PDT) From: Kevin Buzzard To: Homotopy Type Theory Message-Id: Subject: [HoTT] doing "all of pure mathematics" in type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1265_1829955231.1558779124386" X-Original-Sender: kevin.m.buzzard@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: , ------=_Part_1265_1829955231.1558779124386 Content-Type: multipart/alternative; boundary="----=_Part_1266_1257074479.1558779124387" ------=_Part_1266_1257074479.1558779124387 Content-Type: text/plain; charset="UTF-8" Hi from a Lean user. As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others. 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 skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings. 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 involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT. 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 talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, 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 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is. If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics). Kevin Buzzard -- 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/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_1266_1257074479.1558779124387 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi from a Lean user.

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.

I have seen enough of Lean to become = convinced that the pain points would be surmountable in Lean. I have seen e= nough of Isabelle/HOL to become skeptical about the idea that it would be s= uitable for all of modern pure mathematics, although it is clearly suitable= for some of it; however it seems that simple type theory struggles to hand= le things like tensor products of sheaves of modules on a scheme, because s= heaves are dependent types and it seems that one cannot use Isabelle's = typeclass system to handle the rings showing up in a sheaf of rings.
<= div>
I have very little experience with HoTT. I have heard th= at 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 Wednes= day on the pain points involved with formalising mathematical objects in de= pendent type theory and during the preparation of my talk I began to wonder= what the analogous picture was with HoTT.

Everyon= e will have a different interpretation of "modern pure mathematics&quo= t; 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 exa= mple I am talking about formalising statements of theorems involving L-func= tions of abelian varieties over number fields, Hodge theory, cohomology of = algebraic varieties, 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 . Classical logic and the axiom of choice are absolutely essential -= - I am only interested in the hard-core "classical mathematician"= stance of the way mathematics works, and what it is.

<= div>If this is not the right forum for this question, I would be happily di= rected to somewhere more suitable. After spending 10 minutes failing to get= onto ##hott on freenode ("you need to be identified with servic= es") I decided it was easier just to ask here. If people want to chat = directly I am usually around at https://leanprover.zulipchat.com/ (registra= tion required, full names are usually used, I'll start a HoTT thread in= #mathematics).

Kevin Buzzard
=

--
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.co= m/d/msgid/HomotopyTypeTheory/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googleg= roups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_1266_1257074479.1558779124387-- ------=_Part_1265_1829955231.1558779124386--