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.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pg1-x537.google.com (mail-pg1-x537.google.com [IPv6:2607:f8b0:4864:20::537]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 502230d3 for ; Sun, 26 May 2019 12:09:59 +0000 (UTC) Received: by mail-pg1-x537.google.com with SMTP id a21sf1843328pgh.11 for ; Sun, 26 May 2019 05:09:59 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558872598; cv=pass; d=google.com; s=arc-20160816; b=v0NPSFCBN8UOE1Cd4sTYiHXDkEnbaNex/Ifyl8gj4gvQlGTtZx4adkxbLoDxQx7Y7O mIX6Cz/EVFy1mpjBGZ84c9orrYwJvsPKPnAi9kQILrBCbDPEmNn6reZGfaqLjuIfQQmb nRnDzbbXsN3hDuKWjMZ7IxLYk0hZB2NmTciz3v33zQP22wrTDZatwn1sGZG6npPwiFbf sSj5YWmHiH3uV5VbWM8qTm2g7ZznADmXivHRvXuMQviLWpI8/l2ownIFz+Qn6UPOxlh1 g3fI5bqp3dyMRJWNfwuIFJS42sPWSCKXTEm9oWvQsz1Z+gtfUSYe5NGcCXbxjASg8X7e Z0Gg== 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:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature:dkim-signature; bh=8WqpB9WRZ/BiRzikrujOX4gbKjhulsn7R3HiBfX4Yjs=; b=XsNACsDexe34WKnc6Gadzd6TRw/39w7ggSlwth/XrPymi413Wuh16rhQt27RWwh+Kq /5VOVYxhSus9dC1YrzbYnggbxNp7dbS3V9h6lSaoPX4QXEEq9Z8qFQctu1epDfY0x9bu TfXNRW4xITpmmnnt1pT7/akTNKCG9SesUZivryxYs7alKTVj+J4hB6xfFW5QmGXLCzWx DjeU/wJeJzGoFF/yEXYmutCveC+Ub1fjomtR6ofNnIer2Sh9sufPFQtKCkP3KxSWkhT3 zzq0DDEiFg+SHOEC4H19T2w78oib/aJjEdguWkocck0oWlV56GUSz0Clu4a3f7OYoioH Tvjg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RGCj45yg; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b29 as permitted sender) smtp.mailfrom=b.a.w.spitters@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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=8WqpB9WRZ/BiRzikrujOX4gbKjhulsn7R3HiBfX4Yjs=; b=mAL+PMUuJUCz8ZlrpVWGi8R68T0KGI4F03QPRCl9eOSlQfKRjB8iweS7Th3g9dfSQR JXUJ8/uDFyXokK+gY0v90M13gaMqbcjGDVbdyN8anZsrJR/oPwvmtQxq/HUh6VBXds8M b4oaNLseWVZ+gxiDdyj7Tn8fu0eW+wJwVlMjDxK4lBNl4rgmvc5HhiqMsi2F6AJJz0rT WmcWwmAE7InIsTj7qFyuUBXS+/5hAg3Vmm5Bpcu6fug0dJqXZp4IDqIMtkL+hzAySbUd RlgYA8bWMMBTU2kezIz+snLQyHj0rCqNm+NlH7SsQmZamuyfbQI3sd67NHF/RQTYgXAc QPxA== 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=8WqpB9WRZ/BiRzikrujOX4gbKjhulsn7R3HiBfX4Yjs=; b=fBznTjMsCnB67GRe92uYDwsUUTMlkzV3pba2C0cLJG1MYxMuVZ5k5fdKI40wK84WrZ mg+1eBTBg6e9agOUtJs4twhWC0aluJcTx1pVvQ0U1A2h0U7R7+j9eg5wJCC2nBkyHRAW ElTpxakksCuqwyGqARwGakziFKFYPzHlrJTKkb2kXBNj5sz/TqT7y5CK9PpSQrRvLwbr MOqBqyRdiAS0jvyKzjCn5R/QqTgashwZXmxH9VelCdR9zyo2RGE6ktvhC8jP1mwoS8yO xOvdigiFYnya+uEThUftqdCuu07iWMMy9Z3TpqqqJ7V9oYx2fSv5ZcLnNmbqfUh8BiGs u1fw== 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:content-transfer-encoding :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=8WqpB9WRZ/BiRzikrujOX4gbKjhulsn7R3HiBfX4Yjs=; b=m+KTqVMH661gDRv0s2jF8j6fv1mfnbA++UEFqQL6A09U3I0eVjc6EfTO7rIueuMGt+ OiRfxTs+dQbTflMS6nqah8w/pM2dYIWmqllyBpRW7sA1pjjkgEfABiCR/kV0EoJs2/sN YyCgWkGOSDidTG5KmxK8NSTBewcOYR6Vx42upZM12LsKz3XVD6yFwM3xx9L6Yb6wYes4 tshEgOkU/e3i+GZT8UKpwfNXwIaGk14iVEcE6LSTN/6uKKsO4omnnegjJI1m6wzYYIt5 Fuuq6DbS7WLsricdHDRTFpSAAxe2AX5D0hz2ZdJ2XaI1uom4N0FCvQ9WsICGBMxt9tLU Jibg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUZBvBeMsNJSCECCCzm41EByoMBow6zW3XW+mHMYIFPlkHuL8zx ooOcMumo0+UlZzSkNW1yoXs= X-Google-Smtp-Source: APXvYqwsPVDFPmAChgBKnUF5U23VFP7Ww8A+ciPNHURsgjChMSZ+9LMxizi8pYPaQn0p2Vn4auEr2A== X-Received: by 2002:a65:448a:: with SMTP id l10mr1781697pgq.53.1558872598184; Sun, 26 May 2019 05:09:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:de4d:: with SMTP id y13ls2935691pgi.12.gmail; Sun, 26 May 2019 05:09:57 -0700 (PDT) X-Received: by 2002:aa7:8752:: with SMTP id g18mr4455703pfo.240.1558872597700; Sun, 26 May 2019 05:09:57 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558872597; cv=none; d=google.com; s=arc-20160816; b=rmfNImNVYaS0WTTenR7IaTHExIcVGGzoIKrV+gtv29HgUtATOL0qhbCkBTnY34RIZ4 ZvRKqEapFkBF81xAVvOU5rn8AW2jxg0GjRWvCPGlGYa1/hTHknZJ7pj4olkT9bVTsmOp IzbPpiIdE58WdqClW3jjv66/SQxqOeKSTmed8iC/IfZwTLVVuIPRTEbXQ5YaY67LRnTs 5M1/lEe3BWK/oc1tRXakPvvV0vmdlunk+liQDZ0FSgW3KX89rubePAB3hTndz7Mp6OCU 4GDzRc7xz4cjt97ISFev/WSq3zX1HYIlv47SyyNLyi+vghGQE1i+I25e6cZ2HQzILa+G nPVQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=aEfnYc3C1DUFiTLCiNqVYcNnlQwM+vVJEApCnM0C2mQ=; b=qvsqYIw3n82x8vi+HFEgyKna1EbZZzwmamlE0V9MNjEyw/WDFNit6M4UmYkVCPbQYa YyAloiiYqHrsxIsQDjjPznqeYpAkWeNvQyjCzyo0p2t0BE4YBTxW7VK7Wa9qYzeWqJ1q XlUt7PqsE15oH4Fwp76kjZksdCwT7hKE0Jj3WLqpuxoahL+zlvOaTvqWq/6jkmCGjo6Q 09qZ3LD2ESpauuTSlLOSJFoxjf+SRPTW/lWVRTcYmn0zJWO56bH5RCHj4S8y3eONuSr8 /eXZHEbdMGB7qtFRVxQ4YHusjZhwPGUmECOqVBx5YcHI8LDMTld3trzvUe85L87hr3C8 Lfsw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RGCj45yg; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b29 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yb1-xb29.google.com (mail-yb1-xb29.google.com. [2607:f8b0:4864:20::b29]) by gmr-mx.google.com with ESMTPS id t72si484628pjb.2.2019.05.26.05.09.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 26 May 2019 05:09:57 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b29 as permitted sender) client-ip=2607:f8b0:4864:20::b29; Received: by mail-yb1-xb29.google.com with SMTP id g62so5519292ybg.7 for ; Sun, 26 May 2019 05:09:57 -0700 (PDT) X-Received: by 2002:a25:1f09:: with SMTP id f9mr51726477ybf.288.1558872597180; Sun, 26 May 2019 05:09:57 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> In-Reply-To: From: Bas Spitters Date: Sun, 26 May 2019 14:09:44 +0200 Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Kevin Buzzard Cc: Noah Snyder , Homotopy Type Theory , Juan Ospina Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: b.a.w.spitters@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RGCj45yg; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b29 as permitted sender) smtp.mailfrom=b.a.w.spitters@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: , Dear Kevin, We've been working on making formalization accessible to mathematicians for a long time. E.g. in our formath project: http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath It's a slow process, but I believe we are making progress. You seem to be mixing at least two issues. - HoTT/UF as a foundation - Current implementations in proof assistants. If you want to restrict to classical maths. Then please have a careful look at how its done in mathematical components: https://math-comp.github.io/mcb/ and the analysis library that is currently under development. https://github.com/math-comp/analysis If you went to help connecting this to the HoTT library, it will be much appreciated. https://github.com/HoTT/HoTT Best wishes, Bas On Sun, May 26, 2019 at 1:41 PM Kevin Buzzard w= rote: > > It seems to me, now I understand much better what is going on (many thank= s to all the people who replied) that dependent type theory + impredicative= prop "got lucky", in that Coq has been around for a long time, and Lean 3 = is an attempt to model basically the same type theory but in a way more sui= ted to mathematics, written by someone who knows what they're doing (de Mou= ra). Using nonconstructive maths e.g. LEM or AC etc in Lean 3 is just a mat= ter of writing some incantation at the top of a file and then not thinking = about it any more. HoTT might be more appropriate for mathematics -- or at = least for some kinds of mathematics -- but its implementation in an actual = piece of software seems a bit more hacky at this point ("use Coq, but don't= use these commands or these tactics"), which maybe raises the entry barrie= r for mathematicians a bit (and speaking from personal experience, already = this entry barrier is quite high). High level tactics are absolutely crucia= l for mathematical Lean users. This is one of the reasons that the Lean doc= umentation is not ideal for mathematicians -- mathematicians need very earl= y on to be able to use tactics such as `ring` or `norm_num` to do calculati= ons with real numbers or in commutative rings, and these tactics are not ev= en mentioned in the standard Lean documentation. > > I am a working mathematician who two years ago knew nothing about this wa= y of doing mathematics on a computer. Now I have seen what is possible I am= becoming convinced that it can really change mathematics. In my experience= the biggest obstruction to it changing mathematics is simply that mathemat= icians do not see the point of it, or what it has to offer a modern working= mathematician; they can see no immediate benefits in learning how this stu= ff works. In short, I think type theory has an image problem. Sure there ar= e category theorists who know about it, but how many category theorists are= there in an average maths department? In the UK at least, the answer is "m= uch less than 1", and I cannot see that changing any time soon. I would lov= e to draw the mathematics and computer science communities closer together = over ideas like this, but it's hard work. I am wondering whether developing= accessible databases of undergraduate level mathematics would at least mak= e mathematicians sit up and take notice, but when I look at what has been d= one in these various systems I do not see this occurring. This weekend I've= learnt something about UniMath, but whilst it might do bicategories very w= ell (which are not on our undergraduate curriculum), where is the basic ana= lysis? Where is the stuff which draws mathematicians in? This by no means a= criticism of unimath -- it is in fact a far more broad criticism of all of= the systems out there. Lean 3 might have schemes but they still can't prov= e that the derivative of sin is cos, and Isabelle/HOL might never have sche= mes. I know that Gonthier and his coauthors had to make a lot of undergradu= ate level maths (Galois theory, algebraic number theory, group theory) when= formalising the odd order theorem in Coq, but it turns out that the odd or= der theorem is perhaps not a good "selling point" for mathematics formalisa= tion when you're trying to sell to "normal research mathematicians", and I = don't know what is. I'm now wondering making formalised undergraduate mathe= matics more accessible to untrained mathematicians is a better approach, bu= t who knows. Obviously "AI which can solve the Riemann hypothesis" will wor= k, but that looks to me like a complete fantasy at this point. > > One thing I have learnt over the last two years is that a whole bunch of = extremely smart people, both mathematicians and computer scientists, have i= nvested a lot of time in thinking about how to do mathematics with type the= ory. I find it very frustrating that mathematicians are not beginning to no= tice. Of course there are exceptions. One day though -- will there simply b= e a gigantic wave which crashes through mathematics and forces mathematicia= ns to sit up and take notice? I guess we simply do not know, but if there i= s, I hope I'm still around. > > Kevin > > > > On Sun, 26 May 2019 at 06:50, Bas Spitters wro= te: >> >> There has been progress in making a cleaner interface with the standard = Coq tactics. (Some abstractions were broken at the ocaml level) >> I'm hopeful that this can be lead to a clean connection between the HoTT= library and more of the Coq developments in the not too distant future. >> As it exists in agda now. >> >> IIUC, UniMath does not allow any of the standard library or it's tactics= , or even record types, since Vladimir wanted to have a very tight connecti= on between type theory and it's semantics in simplicial sets. So, I don't e= xpect them to connect to other developments, but I could be wrong. >> >> About the bundled/unbundled issue, which also exists in Coq, there's som= e recent progress "frame type theory" which should be applicable to both Co= q and lean: >> http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_51 >> >> Coming back to Kevin's question, yes, HoTT (plus classical logic for set= s), seems to be the most natural foundation for mathematics as is currently= published in the Annals. >> >> On Sat, May 25, 2019 at 6:42 PM Noah Snyder wrote: >>> >>> UniMath vs HoTT wasn=E2=80=99t exactly my point, UniMath =3D Book-HoTT = is of a category from =E2=80=9CCoq with the indices-matter option plus the = HoTT library." =E2=80=9CCoq with the indices-matter option plus the HoTT = library" is of the same category as "Lean plus the math library" and then i= t makes sense to compare how practically useful they are for math. >>> >>> Here it's important to note that most advanced things that you can do i= n Coq are broken by using the "indices-matter" option and relatedly not usi= ng the built-in type Prop. Quoting from https://arxiv.org/abs/1610.04591 "= This small change makes the whole standard library unusable, and many tacti= cs stop working, too. The solution was rather drastic: we ripped out the s= tandard library and replaced it with a minimal core that is sufficient for = the basic tactics to work." >>> >>> (In particular, I was in error in my previous email, *some* tactics are= available in Coq+indices-matter+HoTT, but not many of the more advanced on= es, and to my knowledge, not tactics needed for complicated homotopical cal= culations.) >>> >>> I should say I've never used Coq, just Agda. (When I was using Agda th= e situation was even worse, things like pattern matching secretly assumed k= even if you used the without-k option, and HITs were put in by a hack that= wasn't totally clear if it worked, etc.) So I'm likely wrong in some plac= es above. >>> >>> So I think from a practical point of view, =E2=80=9CCoq with the indice= s-matter option plus the HoTT library" is well behind ordinary Coq (and als= o Lean) for doing ordinary mathematics. However, if and when it does catch= up some of the pain points involving transporting from my previous email s= hould go away automatically. (Side comment: once you start talking about t= ransporting stuff related to categories across equivalences of categories i= t's only going to get more painful in ordinary type theory, but will remain= easy in HoTT approaches.) >>> >>> Best, >>> >>> Noah >>> >>> p.s. Installed Lean last week. Looking forward to using it next year w= hen Scott and I are both at MSRI. >>> >>> On Sat, May 25, 2019 at 11:36 AM Kevin Buzzard wrote: >>>> >>>> Hi Noah. Thank you for pointing out the category error. It seems to me= that sometimes when I say "HoTT" I should be saying, for example, "UniMath= ". >>>> >>>> Tactics in Lean are absolutely crucial for library development. Coq ha= s some really powerful tactics, right? UniMath can use those tactics, presu= mably? >>>> >>>> I understand that UniMath, as implemented in Coq, takes Coq and adds s= ome "rules" of the form "you can't use this functionality" and also adds at= least one new axiom (univalence). >>>> >>>> On Sat, 25 May 2019 at 15:50, Noah Snyder wrote: >>>>> >>>>> I=E2=80=99d also imagine that a =E2=80=9Cpractical=E2=80=9D implement= ation would likely have some kind of =E2=80=9Ctwo-level=E2=80=9D type theor= y where you can use types that behave classically when that=E2=80=99s bette= r and HoTT types when that=E2=80=99s better. >>>> >>>> >>>> But plain Coq has such types, right? >>>> >>>> OK so this has all been extremely informative. There are other provers= being developed which will implement some flavour of HoTT more "faithfully= ", and it might be easier to develop maths libraries in such provers. >>>> >>>>> For example, if G and H are isomorphic groups and you want to transla= te a theorem or construction across the isomorphism. In ordinary type theo= ry this is going to involve annoying book-keeping which it seems like you= =E2=80=99d have to do separately for each kind of mathematical object. >>>> >>>> >>>> Yes. This is a pain point in Lean. It's a particularly nasty one too, = as far as mathematicians are concerned, because when you tell a mathematici= an "well this ring R is Cohen-Macauley, and here's a ring S which is isomor= phic to R, but we cannot immediately deduce in Lean that S is Cohen-Macaule= y" then they begin to question what kind of crazy system you are using whic= h cannot deduce this immediately. As an interesting experiment, find your f= avourite mathematician, preferably one who does not know what a Cohen-Macau= ley ring is, and ask them whether they think it will be true that if R and = S are isomorphic rings and R is Cohen-Macauley then S is too. They will be = very confident that this is true, even if they do not know the definition; = standard mathematical definitions are isomorphism-invariant. This is part o= f our code of conduct, in fact. >>>> >>>> However in Lean I believe that the current plan is to try and make a t= actic which will resolve this issue. This has not yet been done, and as far= as I can see this is a place where UniMath is a more natural fit for "the = way mathematicians think". However now I've looked over what has currently = been formalised in UniMath I am wondering whether there are pain points for= it, which Lean manages to get over more easily. That is somehow where I'm = coming from. >>>> >>>>> >>>>> For example, say you have a theorem about bimodules over semisimple = rings whose proof starts =E2=80=9Cwlog, by Artin-Wedderburn, we can assume = both algebras are multimatrix algebras over division rings.=E2=80=9D Is th= at step something you=E2=80=99d be able to deal with easily in Lean? If no= t, that=E2=80=99s somewhere that down the line HoTT might make things more = practical. >>>> >>>> >>>> This is a great example! To be honest I am slightly confused about why= we are not running into this sort of thing already. As far as I can see th= is would be a great test case for the (still very much under development) t= ransport tactic. Maybe we don't have enough classification theorems. I thin= k that our hope in general is that this sort of issue can be solved with au= tomation. >>>> >>>> Kevin >>>> >>>> >>>>> >>>>> But mostly I just want to say you=E2=80=99re making a category error = in your question. HoTT is an abstract type theory, not a proof assistant. >>>>> >>>>> Best, >>>>> >>>>> Noah >>>>> >>>>> On Sat, May 25, 2019 at 9:34 AM Juan Ospina wro= te: >>>>>> >>>>>> On page 117 of https://arxiv.org/pdf/1808.10690.pdf appears the "add= itivity axiom". Please let me know if the following formulation of the suc= h axiom is correct: >>>>>> >>>>>> >>>>>> >>>>>> >>>>>> On Saturday, May 25, 2019 at 5:22:41 AM UTC-5, awodey wrote: >>>>>>> >>>>>>> A useful example for you might be Floris van Doorn=E2=80=99s formal= ization of >>>>>>> the Atiyah-Hirzebruch and Serre spectral sequences for cohomology >>>>>>> in HoTT using Lean: >>>>>>> >>>>>>> https://arxiv.org/abs/1808.10690 >>>>>>> >>>>>>> Regards, >>>>>>> >>>>>>> Steve >>>>>>> >>>>>>> > On May 25, 2019, at 12:12 PM, Kevin Buzzard = wrote: >>>>>>> > >>>>>>> > Hi from a Lean user. >>>>>>> > >>>>>>> > As many people here will know, Tom Hales' formal abstracts projec= t https://formalabstracts.github.io/ wants to formalise many of the stateme= nts 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 point= s, 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 poin= ts would be surmountable in Lean. I have seen enough of Isabelle/HOL to bec= ome skeptical about the idea that it would be suitable for all of modern pu= re mathematics, although it is clearly suitable for some of it; however it = seems that simple type theory struggles to handle things like tensor produc= ts of sheaves of modules on a scheme, because sheaves are dependent types a= nd it seems that one cannot use Isabelle's typeclass system to handle the r= ings showing up in a sheaf of rings. >>>>>>> > >>>>>>> > I have very little experience with HoTT. I have heard that the fa= ct that "all constructions must be isomorphism-invariant" is both a blessin= g 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 poi= nts 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 mat= hematics" so to fix our ideas, let me say that for the purposes of this dis= cussion, "modern pure mathematics" means the statements of the theorems pub= lishsed by the Annals of Mathematics over the last few years, so for exampl= e I am talking about formalising statements of theorems involving L-functio= ns of abelian varieties over number fields, Hodge theory, cohomology of alg= ebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the li= ke; one can see titles and more at http://annals.math.princeton.edu/2019/18= 9-3 . Classical logic and the axiom of choice are absolutely essential -- I= am only interested in the hard-core "classical mathematician" stance of th= e way mathematics works, and what it is. >>>>>>> > >>>>>>> > If this is not the right forum for this question, I would be happ= ily 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 requi= red, 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 Googl= e 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.co= m/d/msgid/HomotopyTypeTheory/a57315f6-cbd6-41a5-a3b7-b585e33375d4%40googleg= roups.com. >>>>>>> > For more options, visit https://groups.google.com/d/optout. >>>>>>> >>>>>> -- >>>>>> You received this message because you are subscribed to the Google G= roups "Homotopy Type Theory" group. >>>>>> To unsubscribe from this group and stop receiving emails from it, se= nd an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>>>>> To view this discussion on the web visit https://groups.google.com/d= /msgid/HomotopyTypeTheory/18681ec4-dc8d-42eb-b42b-b9a9f639d89e%40googlegrou= ps.com. >>>>>> For more options, visit https://groups.google.com/d/optout. >>>>> >>>>> -- >>>>> You received this message because you are subscribed to the Google Gr= oups "Homotopy Type Theory" group. >>>>> To unsubscribe from this group and stop receiving emails from it, sen= d an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>>>> >>>>> To view this discussion on the web visit https://groups.google.com/d/= msgid/HomotopyTypeTheory/CAO0tDg4dyjZHueTPQEYKQaojSw6SDKNUC8y49JHMoR9oTQOmM= w%40mail.gmail.com. >>>>> >>>>> >>>>> For more options, visit https://groups.google.com/d/optout. >>> >>> -- >>> You received this message because you are subscribed to the Google Grou= ps "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/ms= gid/HomotopyTypeTheory/CAO0tDg7LAv8A%2BoXRLhsN3O7uXCh3D%2BSfBSsr-hmwRsr1iwz= tPg%40mail.gmail.com. >>> 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/CAOoPQuTnM2F9a5VTGKjfxemPCizRyiAoM_VDYNgfTnF89gCBKg%40ma= il.gmail.com. For more options, visit https://groups.google.com/d/optout.