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-ed1-x53a.google.com (mail-ed1-x53a.google.com [IPv6:2a00:1450:4864:20::53a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e48b3d44 for ; Sun, 2 Jun 2019 17:49:31 +0000 (UTC) Received: by mail-ed1-x53a.google.com with SMTP id y24sf23596947edb.1 for ; Sun, 02 Jun 2019 10:49:31 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1559497770; cv=pass; d=google.com; s=arc-20160816; b=lNOEjZRGFgj96+y5ANzJ3UBLkSKhGV1/gt83scSEWKLaFnAW70SylaXyw1x9nXLTmh HnR6Wl4ihVWyu2WC+oGbU7cDDrUWZ95nu6agZyO5kNCEm4mnYl/f1KgPywEa8vhC/9Kb iVSQSQVyCYK+3uJG2XzVG9uCRx3zvgWjmmOp4WkF0JIXNNw12+JYCK1wNwxBAvYzGXlG f13C4x8c1ye/T3juk/1PTR2orxLO7niSfAKAuejXxP8lMhhk43XLZJpw3JrS+CPfnE27 9X/JdvwE4XeguCcO0Bl611g9QlCS8fiflIaDTfS8sTTaF5jbfxZQx3b9LK9qyAjsZPnx 2izQ== 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=BFuJyqo1CRPbrgWytnUHfGYf8YmOyxi8laRwsH+yMW4=; b=mqWGSRAZmhrblzshRtP/DWKoByzqDEtJmiA51vRRfwsHA8EtVib+ynw7GYxtCtHTcQ SxE+zZBcuAnIqA67F7HraBQluYHKnlE0MpZVhffs85YxW2DDWJ2ffyFpMwcUrlPOHo2E 1lycr7lukTegNy8gzYHE0ZuRVqmXh6UxZ2bFkc5I++aGCVYlLOQqMSVfrK2vGeboPy6Y n+fekgrGwXy6JrUckZ4KrOXng26YaWsRFJ+PFr9jGgDt2siMOa+DWjkU3oYOMaR/X0DM Ig4HnYczb80NCvdiG2+fo0SSgmwIXy7raV8WD2xRvYiLLJdidgfe+uGl9Qkc6JOiUuH0 eb7g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=qCaB3vl0; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::242 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=BFuJyqo1CRPbrgWytnUHfGYf8YmOyxi8laRwsH+yMW4=; b=WjCOgXCAuDHbWZ1KMncQT4FWLE2w6Zx/5JRhr9zCAGNPmFAjASRAQjrw3dtfQmjQEB xXasIcFuNql2j6E3aSxiPRtLmiULfGL3/7u5dUJoMCbV3QNM65nofymvkIEleqFYA1Pr jByh2erLxwhq/EBzkjDRynvg5E+sXo9goeiuMyJ5u+9L35vGPXslJXwbyxxqXIDzBY6y I6EtP5/cjkL2QWhDFOc4H8/QENBth5JUbMne9GieDWj9RbkaMp/Frb1NgNq1zHAc0NQO izV7DnxDv2uc2QhXCXu6ajcZxcHt7uNxPU4EXg5P7pB9Oc+Pxscra4Aqcm1ecCUG9B93 MAXg== 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=BFuJyqo1CRPbrgWytnUHfGYf8YmOyxi8laRwsH+yMW4=; b=IEfiOEyb7kGRdGuuEto11GrhDUlCJ6WQZ0kJp8SF5mpO0VChnsIg3QeWg418u1/JXT PBSvGJbHRuv2mATviTlOROtrOJiFjyIUTZvJVjStZL70VhVvvvVcpkMRPaggb0Aor2jD RAvZ2dFsgHxOGIPmKHioxIJPXX/5xInElpQBXl4BriN0nCZqBATNMoRiZfhsDsNNQ8Uk nB3J5xfLwosjCneAN8Xu9Ana0+vQeEBUB2u12zZ1Abxpt494SPIkZ6xvNQwzNTIgUbMm q2BSrA/jDmqDAyqfuRNFn2kHA0w2NhJXSKxWwnyZWTWR8QDPAVPmuE6e3InFFDJkyLqd VN9Q== 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=BFuJyqo1CRPbrgWytnUHfGYf8YmOyxi8laRwsH+yMW4=; b=p0tCwVeCWQYVoyKE6AbQTcG3GP93BRcGcBRKHthkJ3JRYvQOfKHeObZCw4AQXcB5SU WLr0DxMtPYODC38P3qtHBF9guTXZsGMY59OhN1dbTvvYbmro8ZI5c5pzGpsYewW222Ft r+M/nsDgFiYJ48WsztBDCQwvUaqQTTXnrpCMC1dQyboOY533B+YVFH1a0z5ZJicJ7BuH DIHdOSOEWrb17D79m77++nsFIyqYhTs0rtcdsHTubCVh7MhmciEqDyZ4Ur/QzGyzcrwo LMkPFqOfJvoxal39WG0HfbQmH6F2z4HUznnplsYmsdogntE5+nVBTQImtiweA+forfrU foDw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXCyPpHvI1IZT3k0IIko5s6pBiR6LH15pIoT9BmUhqY7pBmBimD Y83NsMP5wQnF9yke+YdqkSQ= X-Google-Smtp-Source: APXvYqzOK56RMErpUIZ4wuFtPC2o84/kpYZh1fH7inNcDHQi+gYwfDhNr/D2/gKaTnXjceqewMWg7g== X-Received: by 2002:a50:87b5:: with SMTP id a50mr23701128eda.118.1559497770335; Sun, 02 Jun 2019 10:49:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6402:185a:: with SMTP id v26ls4158673edy.8.gmail; Sun, 02 Jun 2019 10:49:29 -0700 (PDT) X-Received: by 2002:aa7:c4d2:: with SMTP id p18mr24275256edr.232.1559497769764; Sun, 02 Jun 2019 10:49:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1559497769; cv=none; d=google.com; s=arc-20160816; b=wXpWq1/zUSkaW6PEjHQsrQNs0odn0byFBtwidxYr9xxB+p2ITG7hgGVvD9ChK7MY2T x2mKKNl56QqIRVh2fQDv670HG2ejyBuBbvyiVwyjygV3HRQAR4VVKTfVXWOLZPclSPo1 FHe/yGRIKF1Zd5VxnVp0RmYhlV7xFGhmZIfwKhmUgVe2LqkUhH7mzdLv2yvN4sJLFrvk a17RLYhCrvbAAW6k4W/nvkY9rFJd+iAD4ZTsha5y/wzMOFrtLPyn68DsQgl6ZhUF/XH8 mZfNU/roVw+0qEkdgr6iv8ILSGgb7MU8xKRjVQWJtxueAea11KmqWix8vw9fhNMdYAmk Q/Wg== 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=q0Et+tWuMIuPaTsEL4WbVlhIBNvDe0CHDt3Yw6ZlUPM=; b=l1wXSPI6WruYriWDN38lQ5MVr7MUuUEJJAZ4kUPJiBCkrnDCR9Oai3i+U9r9jH0K0+ nl3HQz2bOTLYxPcCHhTbp+JTEUqehJ1HVcxWjGSdMoF0uiF5HfyW38WqM8fE+p4dXU7w 4PKwfhQNOKpwigDdizPT+Ej1brqAoGEzOit1FwAw9T6RrdSGEQ4RnEXR7jRio5y30f7I Py+pkEKPK8DcWXPP5mShw1wfUWGlqxVtQaYm57xAltH+N5Qq+SrOewW1FlvUVrpYgs5f czCqVAgGoblpGevwNSoIr+3hQb1US1LqEn1m+ctIcC863jmT8hkppHn5Y3+t8zE79IK+ dENA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=qCaB3vl0; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::242 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-x242.google.com (mail-lj1-x242.google.com. [2a00:1450:4864:20::242]) by gmr-mx.google.com with ESMTPS id o1si143566edc.2.2019.06.02.10.49.29 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 02 Jun 2019 10:49:29 -0700 (PDT) Received-SPF: pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::242 as permitted sender) client-ip=2a00:1450:4864:20::242; Received: by mail-lj1-x242.google.com with SMTP id m15so5754436ljg.13 for ; Sun, 02 Jun 2019 10:49:29 -0700 (PDT) X-Received: by 2002:a2e:818b:: with SMTP id e11mr11768445ljg.82.1559497769480; Sun, 02 Jun 2019 10:49:29 -0700 (PDT) MIME-Version: 1.0 References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> <3f6331a7-688e-570b-01d8-d02a81eac96b@inria.fr> <9232f85a-6d64-84dc-a2d0-290c0fc6e760@cse.gu.se> In-Reply-To: From: Kevin Buzzard Date: Sun, 2 Jun 2019 18:49:12 +0100 Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: Michael Shulman Cc: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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=qCaB3vl0; spf=pass (google.com: domain of kevin.m.buzzard@gmail.com designates 2a00:1450:4864:20::242 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: , On Thu, 30 May 2019 at 18:14, Michael Shulman wrote: > > Thanks Martin! Of course you are right that there are people who > don't need to be convinced and who derive benefit and pleasure from > their formalization efforts, and in our community we probably > encounter a lot of them. However, I still maintain that the *average* > working mathematician is not yet going to find such work useful or > rewarding for its own sake. If you go to, say, the U.S. Joint > Mathematics Meetings and stop a hundred mathematicians at random in > the lobby and ask whether they have ever formalized their work in a > proof assistant, how many do you think will say yes? I think this is absolutely right, and an important point. We can even go further: ask 100 mathematicians whether they have ever formalised *anything at all* in a proof assistant, and only epsilon will say yes. This is why I am focussing on the undergraduates. What we as a community can offer undergraduates is a guarantee that a proof is correct; one could regard this as "instant feedback". I think it is currently very difficult to answer the question I've been asked by several staff members -- "what is in it for me"? Some people might find this a negative approach, but if computer proof systems are introduced in undergraduate curricula, and the response to the question "what is the point of teaching these people type theory?" can be something like this: "what is the point of teaching them Banach spaces? Some will use it later on, many won't. Many students graduate, leave mathematics, and never really use these high-powered objects again. For those people, a course on type theory will teach them just as much as a course on Banach spaces -- it will just give them another domain where they can reason logically, learn some easy theorems, learn some deeper results, etc. Oh, and there's evidence that one day type theory will change the world in a way that Banach spaces probably will not". This is the line I am going to take in a couple of years' time when we are discussing changes to my university's curriculum. And then in a generation's time, one can hope that more than epsilon will say yes. Mathematical culture sometimes changes very slowly. We might be using different systems but I still believe that we are looking at the future, and if the current staff can't see it then we have to work on the future staff. The problem I find with this evil plan for world domination is that most senior people I talk to (across all of these systems) tend not to be employed by maths departments. This is a different issue, which needs different ideas, but those are really orthogonal to this conversation. The thing I know for sure is that there are modern maths undergraduates who grew up with computer games and who find the idea of turning their example sheet questions into levels of a computer game quite appealing. Kevin > > Perhaps I am too pessimistic. But let me in turn offer myself as an > example: in addition to being a homotopy type theorist, I have another > hat as a classical category theorist and homotopy theorist. When I > prove things in HoTT, I often formalize them in a proof assistant. > But when I prove things in classical mathematics, I very rarely > consider formalizing them. Only once have I formalized a proof in > classical category theory; the experience was more time-consuming and > less enjoyable than I expected, and I have no plans to do it again. > And I expect that as classical mathematicians go, I am (even when I > have my classical mathematician hat on) pretty far on the > sympathetic-to-formalization side of the spectrum. > > > > On Wed, May 29, 2019 at 12:05 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 > wrote: > > > > Thanks for this discussion. I like it. > > > > Maybe I would like to argue with this point: > > > > On 28/05/2019 10:50, Michael Shulman wrote: > > > I think it's fairly hopeless to convince a classical mathematician > > > that they should put in a lot of work to convince a computer of the > > > truth of *something they already knew*. > > > > I am not sure why the person who started this thread, a mathematician, > > Kevin Buzzard, decided to put in such a lot of work, but did and he > > has (in Lean), with his students. > > > > But having interacted with a lot of students (from my institution, and > > from everywhere in the world, from maths, logic, computer science and > > philosophy departments (and once even a high school student in the > > UniMath School)), what I can say is that they are not trying to > > convince the computer. > > > > They are trying to convince themselves, using the computer to both > > check their understanding and record their understanding when > > the proof is complete. > > > > If I am allowed to speak for myself, I created a univalent library in > > Agda for the purpose of *doing something else*. However, it is nice to > > stare at the library and see everything developed from first > > principles. When presented with the mathematical literature, both as > > students and experienced mathematicians, we are never sure how far > > back one has to read until everything begins in a precise way. How > > much have we created, and how do all the different fields of > > mathematics interact with each other? When one records mathematics in > > the computer, this begins to become clear, or at least the asnwers to s= uch > > questions become possible. > > > > We don't need to *convince* anybody. This will *happen*. And it is > > already happening. The students like it. This is my experience. > > > > M. > > > > > > -- > > 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/c7197bc2-7fc5-4027-bed6-24b2d350950f%40googlegroups.= com. > > For more options, visit https://groups.google.com/d/optout. > > -- > 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/CAOvivQxAZEXiCSS5%2BipOszo%3DJeymDXL3jyfuNFdY7AKxAZSS4= g%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/CAH52Xb0SKwTaKtkBdZgav3KPkrqGs-eYae11v103ErYU%3D2dCRQ%40= mail.gmail.com. For more options, visit https://groups.google.com/d/optout.