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=-0.8 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-wr1-x43b.google.com (mail-wr1-x43b.google.com [IPv6:2a00:1450:4864:20::43b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 55b423aa for ; Sun, 24 Nov 2019 18:11:19 +0000 (UTC) Received: by mail-wr1-x43b.google.com with SMTP id t9sf3298297wru.10 for ; Sun, 24 Nov 2019 10:11:19 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1574619079; cv=pass; d=google.com; s=arc-20160816; b=ZcMFqK+M9motQrZ7EgPRjEdUXtq3i3QZ/XOnyAtIZp2By3YttDFqvZyO0z07L7pchW S1Inug/aevM8VRZV3m9ZnVWj9Dg/BSMQOnDXy9YH9DomIQRFP5QELl8udoH/MW12J0Yw zmC5O9nnLeP+Fmis03RI/DH7a5+mt5TaDtDbOrj70pGKxYx8ZEICwpUlQZiF17dwDAUg pLZ4ObRufQGtTbOHLnKg2sleqUsgUnowUqN0V6B9dZOx97pNR+hy2qg4dHT/3GGXxy1w hq6XVOgK84bnY+kXjC1OnkQGEyLA7VMBOXbY2JstqPc60O+TVHZ8b2/KPmZ+KNC7iSm0 +odg== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=1HaCDXYa17wsfYogdFJYRe4lFcV6H8mw6jNn7uXqdv4=; b=cRp2H4ojfhRECiUNeW42wZ0ejY5mzRO8KKAKkQMfh+/J+VHFgFqa9h1kYZFb4Ki8cT 3eMgJu3om1wvWzYrldFefKWPbcDrxJkn42aVu9Mqpv7tz3pvjOiBxxOndxXqq5okSNIc Kbzq3tVEjHlnMDrffZl+0EsXXbxHqxlB+3bvlPMgvpH+ZtbW9P0bZVYwQHIgTbiYlyBT rKkuXvhO6QtzVAxVZ5qmAmccGc7hFvtrj/YdlHFnDH0ZHavZVGsyAJOn6bsZ+SRUm4Q4 fz0iEcxzZDC+4T6MyRyfi36w6q/OUKGA91qToA44ywInEM4SuAVhv5OVJlnF67vgekmk GCcQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="n/F0flFD"; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::232 as permitted sender) smtp.mailfrom=kevin.m.buzzard@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=20161025; 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-unsubscribe; bh=1HaCDXYa17wsfYogdFJYRe4lFcV6H8mw6jNn7uXqdv4=; b=AdpkMvMmAMym3gLsQYNOZp5T0FGEAfHNjV7qRsZr3hc4RmiBWN1CER5p/BaeYdV2o4 voxscQEOuT+AdLmMTTYgNvmrdNRK62TrhPESKnpkblCgY+5mrPHcIuVCSX3xBFDi0Ge7 lzpN3Iw1pHNW7bwq3XgFdwIcRw0HhYQHBUlvN+AuV9nzRr4opi2GaDfBqDsZqFexyPGK ZMoUDHUuJXCsx0YS9HLCF7LomUQ4VYXILRavI/glrCE+jfkmvqO2fJnchBC/INCzgICA wWLPG6A+LXPNv91EebKI/+WG2v4xICBWv+3QRwyc0d0Y+MCR1DgQsKi7ITXWoPuVHo5l 7cCg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; 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-unsubscribe; bh=1HaCDXYa17wsfYogdFJYRe4lFcV6H8mw6jNn7uXqdv4=; b=D2KQVT/ZxWk5PuuqoZL7d5X5OetLLJrfPhHObJBqA0DaxCfs5WKb7M9ZQnjpO7sEYA k6qlBvoPGWEZPo6op/fw32Xnnac/74FIChgGyi3MW0P4AXTUkRmg6fHrZXjInmAO+ky3 Q94bS3FkSUplr6CLIqhIbaXBmOqwvq0cZvC7SuEecf9wSH7q8OaFU2W7ztyMBSxMPxfi s+ola0hZqvZiX+5uDsfAtAIN2aSVwGx3z4/GQxYKUIVq61rsDFQqdxjXhj9o3fEZgvYZ uGGSf4/rGOMSbpu9dp0HYdp3AW5qgYtLzBQDT8/sALzjBAz9rkVEjKFJwAaqsmKZy1cn mYHA== 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: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-unsubscribe; bh=1HaCDXYa17wsfYogdFJYRe4lFcV6H8mw6jNn7uXqdv4=; b=E2J5L6471ixI6IKmkYNDpZ+Nn8yrb3i1Wu9pzbYcXe1nBsoicvGreOK1ryWOgHsYT0 InMmoi+LqP9AlRajKO22uxtFcgpEWpptZDMz4wypOE/zWWHNcUCFgSXE4tx9o5AID1wp SlnVIbs/dklCDX7Ed1Oslcn+F8lT2JJGgh9Np2TnFQ1Rn2JiXITBNssDvs71xldFE2Hp AF00uhBqF/k/x84c022EOtP40YmINQo8yw7m+hXLJZTyjmZYdG82sNCX0GOAFjlhyQya pgGU1rckEvYj6idAa14NeIZ4JUoC9CNvtv71ZV01hH0/4aPQHG7iQKAxIWoKB5hbSiH0 Ga5w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWBbw/uPht8Tx89xwoAhthO7+ayjkKXTDZsBtOVOxEXWI+K/52y FCRtRz+roXxgv093cW/nH4c= X-Google-Smtp-Source: APXvYqybISXz+ZP4Z4r8JaIlctON2+1MCDEdxjmFhOTAhOfR8OKYcAE8R5r8ukuLTZak+VfShkgAdg== X-Received: by 2002:a7b:c0da:: with SMTP id s26mr25248218wmh.6.1574619078839; Sun, 24 Nov 2019 10:11:18 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:5382:: with SMTP id d2ls6304920wrv.6.gmail; Sun, 24 Nov 2019 10:11:18 -0800 (PST) X-Received: by 2002:adf:ef51:: with SMTP id c17mr29700711wrp.266.1574619078040; Sun, 24 Nov 2019 10:11:18 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1574619078; cv=none; d=google.com; s=arc-20160816; b=PXqjGMdIAclMpbwlgTEaWcdpcnL5vYmcDRBGA78Q9QOyfr514wGKYN8oiiiWqzOazp hqZU6geOLecObc545mIO/9jJnFmjUF2ScqBccggL1ltXcHUoXHSsT3cjPE/Zthl853Yl lUAqolE8zpoMG3be9MkLeTQTz1RXud+fMNfvnItKiJan2awMjd6jKLz/4MGUachHSRfg K+STaSHs6vzRA0I1KP0D4lEWQSltNVJ38bQ0IavhTa4rhajcCG8oDaaSKm2n5cK+uA9B oYvNSuD3YjeTLkPhpzyaxSAhvGdB7PFgdb3Fw0BiPYyE6End1XzCCk9S3ElmB5iNHqU7 ZvGg== 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=S0ZvNH7CZE0j/Y5vqX19aIJOt4Vy2ibrt43wv66hzp0=; b=Pt5Ae5QROIYP6mDOG7rD9eK0jjsNsxzRQTjI4lJQc8GoZNDkx/kf3HApeMNR4xpmsP b/07pNxt9ranz4Rfnp4ttKqdlzAfO35Ln8TYnQiJw7mUl4xBOBEBcBzb7xLpZecZun0C JIiZ3kk2yhySiXQed0IfI8Q023nHiFuT/SI81h3hqeH1G0E5VlZyJR6iUwqeQa8CB+QV EBC94jMLmFA4HvthyBKVWjeW1NR3RliUKB+OAaXZyjwkK+6MaEEh9405RM3xCuw4Rl86 VPlDe3ggwhvJODsaBgXkWOO3zhy726IeH9AbT5Jdvetbl+E4PjKn1YlsmZ/piMAvAaEr lcJg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="n/F0flFD"; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::232 as permitted sender) smtp.mailfrom=kevin.m.buzzard@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lj1-x232.google.com (mail-lj1-x232.google.com. [2a00:1450:4864:20::232]) by gmr-mx.google.com with ESMTPS id i13si184230wru.2.2019.11.24.10.11.18 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 24 Nov 2019 10:11:18 -0800 (PST) Received-SPF: pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::232 as permitted sender) client-ip=2a00:1450:4864:20::232; Received: by mail-lj1-x232.google.com with SMTP id g3so13033112ljl.11 for ; Sun, 24 Nov 2019 10:11:18 -0800 (PST) X-Received: by 2002:a2e:7319:: with SMTP id o25mr17532059ljc.207.1574619077671; Sun, 24 Nov 2019 10:11:17 -0800 (PST) MIME-Version: 1.0 References: <2ca6c47c-6196-4b45-b82c-db79b2b6568c@googlegroups.com> In-Reply-To: From: Kevin Buzzard Date: Sun, 24 Nov 2019 18:11:01 +0000 Message-ID: Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? To: Nicolas Alexander Schmidt Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000c801c105981b92c8" X-Original-Sender: kevin.m.buzzard@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="n/F0flFD"; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::232 as permitted sender) smtp.mailfrom=kevin.m.buzzard@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: , --000000000000c801c105981b92c8 Content-Type: text/plain; charset="UTF-8" > Kevin, I would like to second Michael's interest in seeing these 20 > commutative diagrams. Moreover, I'd also be very interested in seeing > your "spaghetti code" (quote from the slides of your Big Proof talk): it > seems it should be informative to see where your initial approach went > wrong, and how much these problems and their solution had anything to do > at all with the formal system you were working in. Are your original > files perhaps available somewhere? > Sorry for the delay. My original repo with a "bad" theorem is here: https://github.com/kbuzzard/lean-stacks-project The bad theorem is this: https://stacks.math.columbia.edu/tag/00EJ The problem is that the rings denoted R_{f_i} (localisations of rings) are typically defined to mathematicians as "this explicit construction here" as opposed to "the unique up to unique isomorphism ring having some explicit property" and, as a mathematician, I formalised (or more precisely got Imperial College maths undergraduates Chris Hughes and Kenny Lau to formalise) the explicit construction of the localisation and then the explicit theorem as stated in the stacks project, not understanding at the time that this would lead to trouble. When I came to apply it, I ran into the issue that on this page https://stacks.math.columbia.edu/tag/01HR we have the quote: "If f, g in R are such that D(f)=D(g), then by Lemma 26.5.1 there are canonical maps M_f->M_g and M_g->M_f which are mutually inverse. Hence [we can regard M_f and M_g as equal]". This is a typical mathematician's usage of the word "canonical" -- it means "I give you my mathematician's guarantee that I will never do anything to M_f which won't work in exactly the same way as M_g so you can replace one by the other and I won't mind". As I explained earlier, by the time I noticed this subtlety it was too late, and this led to this horrorshow: https://github.com/kbuzzard/lean-stacks-project/blob/7c2438e441547da6a5786a9a427fd78cbc407fa9/src/canonical_isomorphism_nonsense.lean#L268 plus the lines following, all of which is applied here https://github.com/kbuzzard/lean-stacks-project/blob/595aa1d6c5ce5a6fa0259c5a0a2226a91b07d96e/src/tag01HR.lean#L208 . That last link is justifying a whole bunch of rewrites along canonical isomorphisms. These were the general lemmas I needed to prove that if A -> B was a map, and if A was canonically isomorphic to A' and if B was canonically isomorphic to B' and A' -> B' was the corresponding map, then the image of A was canonically isomorphic to the image of A' etc, all in some very specific situation where "canonically isomorphic" was typically replaced by "unique isomorphism satisfying this list of properties". Note that this is crappy old code written by me when I had no idea what I was doing. One very interesting twist was this: the universal property of localisation for the localised ring R_f is a statement which says that under certain circumstances there is a unique ring homomorphism from R_f; however in https://stacks.math.columbia.edu/tag/00EJ the map beta in the statement of the lemma is *not* a ring homomorphism and so a naive application the universal property was actually *not enough*! One has to reformulate the lemma in terms of equalisers of ring homomorphisms and remove mention of beta. None of this is mentioned in the stacks project website because we are covered by the fact that everything is "canonical" so it's all bound to work -- and actually this is *true* -- we are very good at using this black magic word. All of this is fixed in Ramon Mir's MSc project https://github.com/ramonfmir/lean-scheme and the explanations of how it was fixed are in his write-up here https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf Briefly, one crucial input was that the localisation map R -> R_f could be characterised up to unique isomorphism in the category of R-algebras by something far more concrete than the universal property, and Ramon used this instead. In HoTT one might naively say that these problems would not arise because isomorphic things are equal. However my *current* opinion is that it is not as easy as this, because I believe that the correct "axiom" is that "canonically" isomorphic objects are equal and that the HoTT axiom is too strong. I developed some rather primitive tools to rewrite certain statements along certain kinds of isomorphisms with some naturality properties, and mathematicians would be happy with these ideas. I can quite believe that if you stick to homotopy types with the model in your mind as being topological spaces up to homotopy then the HoTT axiom is perfect. However there are things other than topological spaces in mathematics, for example commutative rings, and in my mind the HoTT axiom just looks weird and wrong in ring theory, and I expect it to backfire when HoTT people start doing some serious ring theory. I might be wrong. Part of me hopes I'm wrong, in fact. But this will remain my opinion until someone comes along and formalises the definition of a scheme in one of the HoTT theories and proves the "theorem" that an affine scheme is a scheme (I write "theorem" in quotes because it is a construction, not a theorem). I had the pleasure of meeting Thorsten Altenkirch earlier this week and I asked him why this had not been done yet, and he told me that they were just waiting for the right person to come along and do it. A year or so ago I was of the opinion that more mathematicians should be using Lean but now I have come to the conclusion that actually more mathematicians should be engaging with *all* of the theorem provers, so we can find out which provers are the most appropriate for which areas. By "mathematicians" here I really mean my ugly phrase "proper mathematicians", i.e. people doing algebra/number theory/geometry/topology etc, people who have absolutely no idea what a type is and would even struggle to list the axioms of set theory. These people with their "canonical" constructions (a phrase which has no meaning) are the problem, and they're very hard to reach because currently these systems offer them nothing they need. I wrote a silly game http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ to help my 1st years revise for my exam (and the game takes things much further than the contents of the course), and I'm writing a real number game too, to help my 1st years revise analysis for their January exam. It would not be hard to write analogous such games in one of the HoTT theories, I would imagine. >From what I have seen, it seems to me that Isabelle is a fabulous tool for classical analysis, Coq is great for finite group theory, the Kepler conjecture is proved in other HOL systems, and the HoTT systems are great for the theory of topological spaces up to homotopy. But number theory has been around for millennia and unfortunately uses analysis, group theory and topological spaces, and I want one system which can do all of them. I think that we can only find out the limitations of these systems by doing a whole bunch of "proper mathematics" in all of them. I think it's appalling that none of them can even *state* the Hodge conjecture, for example. For me, that is a very simple reason for a "proper mathematician" to immediately reject all of them in 2019. But I digress. Kevin > > > -- > > Nicolas > > > > > -- > 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/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fromzerotoinfinity.xyz > . > -- 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/CAH52Xb2AoMWBeCCJ5B8%3DDfa8UgmO1vbWf7a%3DdvfRqTFTdu61qA%40mail.gmail.com. --000000000000c801c105981b92c8 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Kevin, I would like to second Michael's interest in seeing these 20
commutative diagrams. Moreover, I'd also be very interested in seeing your "spaghetti code" (quote from the slides of your Big Proof ta= lk): it
seems it should be informative to see where your initial approach went
wrong, and how much these problems and their solution had anything to do at all with the formal system you were working in. Are your original
files perhaps available somewhere?

Sorr= y for the delay.

My original repo with a "bad= " theorem is here:


The bad theorem is this:

=

The problem is= that the rings denoted R_{f_i} (localisations of rings) are typically defi= ned to mathematicians as "this explicit construction here" as opp= osed to "the unique up to unique isomorphism ring having some explicit= property" and, as a mathematician, I formalised (or more precisely go= t Imperial College maths undergraduates Chris Hughes and Kenny Lau to forma= lise) the explicit construction of the localisation and then the explicit t= heorem as stated in the stacks project, not understanding at the time that = this would lead to trouble. When I came to apply it, I ran into the issue t= hat on this page

https://stacks.math.columbia.edu/tag/01HR

we have the quote: "If f, g in R are such that D(= f)=3DD(g), then by Lemma 26.5.1 there are canonical maps M_f->M_g and M_= g->M_f which are mutually inverse. Hence [we can regard M_f and M_g as e= qual]".

This is a typical mathematician's= usage of the word "canonical" -- it means "I give you my ma= thematician's guarantee that I will never do anything to M_f which won&= #39;t work in exactly the same way as M_g so you can replace one by the oth= er and I won't mind".

As I explained= earlier, by the time I noticed this subtlety it was too late, and this led= to this horrorshow:


plus the l= ines following, all of which is applied here


. That last link is justifying a= whole bunch of rewrites along canonical isomorphisms. These were the gener= al lemmas I needed to prove that if A -> B was a map, and if A was canon= ically isomorphic to A' and if B was canonically isomorphic to B' a= nd A' -> B' was the corresponding map, then the image of A was c= anonically isomorphic to the image of A' etc, all in some very specific= situation where "canonically isomorphic" was typically replaced = by "unique isomorphism satisfying this list of properties". Note = that this is crappy old code written by me when I had no idea what I was do= ing. One very interesting twist was this: the universal property of localis= ation for the localised ring R_f is a statement which says that under certa= in circumstances there is a unique ring homomorphism from R_f; however in <= a href=3D"https://stacks.math.columbia.edu/tag/00EJ">https://stacks.math.co= lumbia.edu/tag/00EJ the map beta in the statement of the lemma is *not*= a ring homomorphism and so a naive application the universal property was = actually *not enough*! One has to reformulate the lemma in terms of equalis= ers of ring homomorphisms and remove mention of beta. None of this is menti= oned in the stacks project website because we are covered by the fact that = everything is "canonical" so it's all bound to work -- and ac= tually this is *true* -- we are very good at using this black magic word. <= br>

All of this is fixed in Ramon Mir's MSc pr= oject


and the explanations of how it was fixed are in his write-up here


Briefly, one crucial i= nput was that the localisation map R -> R_f could be characterised up to= unique isomorphism in the category of R-algebras by something far more con= crete than the universal property, and Ramon used this instead.
<= br>
In HoTT one might naively say that these problems would not a= rise because isomorphic things are equal. However my *current* opinion is t= hat it is not as easy as this, because I believe that the correct "axi= om" is that "canonically" isomorphic objects are equal and t= hat the HoTT axiom is too strong. I developed some rather primitive tools t= o rewrite certain statements along certain kinds of isomorphisms with some = naturality properties, and mathematicians would be happy with these ideas. = I can quite believe that if you stick to homotopy types with the model in y= our mind as being topological spaces up to homotopy then the HoTT axiom is = perfect. However there are things other than topological spaces in mathemat= ics, for example commutative rings, and in my mind the HoTT axiom just look= s weird and wrong in ring theory, and I expect it to backfire when HoTT peo= ple start doing some serious ring theory. I might be wrong. Part of me hope= s I'm wrong, in fact. But this will remain my opinion until someone com= es along and formalises the definition of a scheme in one of the HoTT theor= ies and proves the "theorem" that an affine scheme is a scheme (I= write "theorem" in quotes because it is a construction, not a th= eorem). I had the pleasure of meeting Thorsten Altenkirch earlier this week= and I asked him why this had not been done yet, and he told me that they w= ere just waiting for the right person to come along and do it. A year or so= ago I was of the opinion that more mathematicians should be using Lean but= now I have come to the conclusion that actually more mathematicians should= be engaging with *all* of the theorem provers, so we can find out which pr= overs are the most appropriate for which areas. By "mathematicians&quo= t; here I really mean my ugly phrase "proper mathematicians", i.e= . people doing algebra/number theory/geometry/topology etc, people who have= absolutely no idea what a type is and would even struggle to list the axio= ms of set theory. These people with their "canonical" constructio= ns (a phrase which has no meaning) are the problem, and they're very ha= rd to reach because currently these systems offer them nothing they need. I= wrote a silly game


to help my 1st = years revise for my exam (and the game takes things much further than the c= ontents of the course), and I'm writing a real number game too, to help= my 1st years revise analysis for their January exam. It would not be hard = to write analogous such games in one of the HoTT theories, I would imagine.=

From what I have seen, it seems to me that Isabel= le is a fabulous tool for classical analysis, Coq is great for finite group= theory, the Kepler conjecture is proved in other HOL systems, and the HoTT= systems are great for the theory of topological spaces up to homotopy. But= number theory has been around for millennia and unfortunately uses analysi= s, group theory and topological spaces, and I want one system which can do = all of them. I think that we can only find out the limitations of these sys= tems by doing a whole bunch of "proper mathematics" in all of the= m. I think it's appalling that none of them can even *state* the Hodge = conjecture, for example. For me, that is a very simple reason for a "p= roper mathematician" to immediately reject all of them in 2019. But I = digress.

Kevin


--

Nicolas




--
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.googl= e.com/d/msgid/HomotopyTypeTheory/bc1a186e-4d33-0296-4b1b-b09ee8188037%40fro= mzerotoinfinity.xyz.

--
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/CAH52Xb2AoMWBeCCJ5B8%3DDfa8Ug= mO1vbWf7a%3DdvfRqTFTdu61qA%40mail.gmail.com.
--000000000000c801c105981b92c8--