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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-vk1-xa3f.google.com (mail-vk1-xa3f.google.com [IPv6:2607:f8b0:4864:20::a3f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3089a362 for ; Thu, 30 May 2019 17:14:47 +0000 (UTC) Received: by mail-vk1-xa3f.google.com with SMTP id x196sf2707973vkx.19 for ; Thu, 30 May 2019 10:14:46 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1559236486; cv=pass; d=google.com; s=arc-20160816; b=pJb00A1h3sdXluBSQrhnI9K5hLdcMcxMq8DwHh/l0FDkLqhg6xVnaCkQ3oa5s+1Ysa tSaiXeHhWZBjAhEnqxFjgeiAKqsHJ1xRPm8+HvM8ZI0GmVjDVJF3kmlJkTEsfyFHomM3 loFJhYJyAP0P/1aqWglHEqpCQXM8ZC7mmPevrIiHvXskoLou3Y6GDSv59o4nVVNusZgl sHlAoVrak/JbM5rifR5PZdh1LUrUPBWC/YM12cAtaUSf78+Z9LpI+dIW+zjadB/a4q72 9rgUtmBWuv53jvR7RrEZH7c+8JPw1fhxxfFsvgAnwCmz8BzdvZfrlLCJOIQKAS7vOIwa TFYw== 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; bh=anRBKBjBpu7vbiH17Y72k3PZZF2e/3DXHANqewUvXQ0=; b=W+AN1IgGqEHumxVG7LEZr5rrWvi3gYQWt7bOhV96G7/6y5OR+sR9wOR4l02W5UvAU1 Mfex695LsiQ/xF9uKnoPocnOYNtnu9gYpwh/rACia/NIx0zhJLSD091fed/xP0O4iar6 6B4W15P3MkSa7CyXt5+o4Bfx3JdpdzDoL7sRKI0+7d7vSU6YC605c3aWNdxffBHkt/ro 2LRohbbupd0j3Xwc/ZJqxS81RIlAhS/GXh53+uS8ltj5ssHysd675TIWAwKtngLzNSY8 q6duies/u332K3a4IGtN2vV5fXgVrMnJctACEBPmkYfT1/Ex80uVFdj5AOJfIWALAoUr gTDQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=KD6b2wKW; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b32 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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=anRBKBjBpu7vbiH17Y72k3PZZF2e/3DXHANqewUvXQ0=; b=aX5eWMbGpZ4WRjRkBRtjmej2iKnZ+NNIeStU5xvQVSXTTYpHCPHInhYNhDJy/m17Is zyaCYehzT3IoZCQwVkRL/Xj5Dym5dgtr50WwR2HtX19GvQEonVXvQormTx4yr4QywK5J 9UphfNb8YbfGxwn9yoHygO9E9Ga6a9JxkzPFx7br+89lYhg6UNBst5AY/mNjZltOCiN6 qlEf3i2uCxIhA73PcHwBoPDsWOuIpWez9UOJmFaXabztupYFZ/0/F7BKwI212ZBNC+uw kcfvQFGcoqgTpJdhJP2ugE/auSGZqJbReE7P4zrpGodoljnH/AJUKYoy6NmxH6DVdpfV AqZw== 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=anRBKBjBpu7vbiH17Y72k3PZZF2e/3DXHANqewUvXQ0=; b=Snpt/zfHp1sggboZCwKVcnb2ctHNKl4aOkj+5RyW9xuEar6SNIlczrVPEyXQv10rcu cMcynzIjFy0ZrAyw/LsGG2gm7iGSxsSZc8M+HVmuxpLEUI4+qXpZ88uqarhiAruaQQhL h6nE87A37vzOaMqAuN9wQ478HBWia8WA5Pf/sP1YrlFrkbJ4tWx1WfVfuL0ORAzuJTF7 n9z1tjaXppTlPS+WMAf8KhWVzxsZ7E9b5qWZPnPp7M7+UE035dTD3KLBGFADVPdVOeFH 59wqxrxnRzwHmEa09cqlk1LtJnVKN/FewB8N+vMJb5groDBTRohKjx6bStbdvPnaI4Hi IM7w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVM85ZLLRb4zB8jv5QlmGUXCe9C2++DlK8pAiNI3n62NtMgqfkB KD31BdympeRuGfpWJuxzjyo= X-Google-Smtp-Source: APXvYqzjYp1iLQvQy/jJFESrMIWpb+/aeCF9Y1FQFL4VO8jOgOVNsyKftfFVLWUE1wyP2nFTjVTNTA== X-Received: by 2002:a1f:9390:: with SMTP id v138mr2039323vkd.48.1559236485810; Thu, 30 May 2019 10:14:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:db06:: with SMTP id s6ls153748vkg.14.gmail; Thu, 30 May 2019 10:14:45 -0700 (PDT) X-Received: by 2002:a1f:aac8:: with SMTP id t191mr1428558vke.2.1559236485366; Thu, 30 May 2019 10:14:45 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1559236485; cv=none; d=google.com; s=arc-20160816; b=nhTUsvG3iSsxkJ9BgC/IyS6/Vet8+rNU5RS7o+n4Cg9Nl1YziiVqVwsG9I+qQ2Emnr JRCeyj0qCXT+35QY+xn5grd36QR4ci1O4HE1iXIKMtvGZ8lfDiHXJFubxDO4/98HyGRG WpeL3HLqnPStLIc6/SyqVHbIY9Lw1ia4X/Qm1DwEn8ZkemKokx6fqNt4xHXs5Q6SBIYa dBwcRKp0TuhzGWrl5ynxXK8h9uf0UnqGqL/ofKTzvVBsGdAchKUzA7Hj5PLcbEnzkhV0 zv0i/ULbQ/oh5G6CTC/uSrqAp1kRbFPBQNRKYV7c8EoxWROmSRp7D9h5sXmvbm1y9xbP 77vQ== 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=iRkXGratQadZAb7f6Qbzkb0uL98FA3PwSsIMvEIeGqI=; b=TPZdhwyBzGhcdXVLpi+NIAMRQLwa1BaIAe7iF5fesq/TZFL7OhbxqcP9Utagzt2trQ 4DX9j9C9MQfvT+8V7/FafkrH0JzVyKiqob9ti5lQvTQoooBtTOYFhg3iwVWA4cncNb9e x9lquXgKg4peimng/TZR6nlKXCwvyZAA7kwPeP80Nga3h/LgTQxqW3FG2XC7oxxXDnTV Sb0c3SFCYMEE180wybdpH3+KTNKXY/DcQn6oL4IWbSGMxfZ0F+Z0tkcIjyRVmZJGZuyj T0Cn0cx92ooCb3zYwhrNUkN1itdsL5gTAUUHGwhznhslh3/vn27quTHeZxKixQjBw5Ws lWCg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=KD6b2wKW; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b32 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb32.google.com (mail-yb1-xb32.google.com. [2607:f8b0:4864:20::b32]) by gmr-mx.google.com with ESMTPS id b9si96113uad.1.2019.05.30.10.14.45 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 30 May 2019 10:14:45 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b32 as permitted sender) client-ip=2607:f8b0:4864:20::b32; Received: by mail-yb1-xb32.google.com with SMTP id x7so2441639ybg.5 for ; Thu, 30 May 2019 10:14:45 -0700 (PDT) X-Received: by 2002:a25:3851:: with SMTP id f78mr2504010yba.236.1559236484607; Thu, 30 May 2019 10:14:44 -0700 (PDT) Received: from mail-yw1-f45.google.com (mail-yw1-f45.google.com. [209.85.161.45]) by smtp.gmail.com with ESMTPSA id 138sm902254ywm.96.2019.05.30.10.14.43 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 30 May 2019 10:14:43 -0700 (PDT) Received: by mail-yw1-f45.google.com with SMTP id t140so2933725ywe.8 for ; Thu, 30 May 2019 10:14:43 -0700 (PDT) X-Received: by 2002:a81:f00e:: with SMTP id p14mr2732848ywm.246.1559236483610; Thu, 30 May 2019 10:14:43 -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: Michael Shulman Date: Thu, 30 May 2019 10:14:32 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] doing "all of pure mathematics" in type theory To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=KD6b2wKW; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b32 as permitted sender) smtp.mailfrom=shulman@sandiego.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: , 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? 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 suc= h > 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 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/c7197bc2-7fc5-4027-bed6-24b2d350950f%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/CAOvivQxAZEXiCSS5%2BipOszo%3DJeymDXL3jyfuNFdY7AKxAZSS4g%= 40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.