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,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x240.google.com (mail-oi1-x240.google.com [IPv6:2607:f8b0:4864:20::240]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 50d99c7e for ; Wed, 29 May 2019 19:04:41 +0000 (UTC) Received: by mail-oi1-x240.google.com with SMTP id c64sf1301244oia.22 for ; Wed, 29 May 2019 12:04:41 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=AIeyZAr2Q8dgdvxDXp519gp0OXgJYNgdTzrV2wN2ZdA=; b=TZ9TXs976PeOy0FvHLCfe729NeBBSKLhYobl1h0gSmkQyUbvI5z4vaF+1UmMipUNYf iJI3PAAZ6a68RVkveXHtI4s8+yFVoq1rVlB6Cag/46aHmwP61u8ENzS25CMqnGId/llr GR88s7OujmWNG2lbVJs6RGCHvEcImoby7pzXnD/1l3ytWrP+B/qvuG0LLYuckERrAiQK XfzS0FqVS4p2AdqwRwX2hbQlT1mA+wsGnyKv6iZRLrvDylglbTOJA/767lqmSBCWQwuP 1YuPZRkGBKLQ1vAeYrFtDMQb3M9iRiO2sat41O6D836ET9K+lF1pBbk8CWxfKUCm3bJ8 xoNA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=AIeyZAr2Q8dgdvxDXp519gp0OXgJYNgdTzrV2wN2ZdA=; b=CZFSXQPM6XL0TpXhoqS5dr1PLrMO6C05aqJ3f51NZSXT4YioOa6PidJ/NCnFTEfwif bC8PSIFOwtlPpzq9SdIljAa1X99M5zEKaw7JFBj8G7gfaXPK1vAn1yYAOVaa5IazD4/E xusoUSaHvTV4uSFEtW4PUWGLHHxgMwmZxC7fTjajQJ8VgYRD2MBlFfh2SNo+Mp9TX92X u+59+BBoiE6npgFHFq8qUsanvewrqIJpofrXev0YCsvYPnW9QEEvYtPyO6Kh7pPH2QFl opNBsQ9HgKtwe4MpiF1QEaVZVcbYIEypRaTXBq2FR/+4vUSGpX2lekbfwcs0iRNqOCvd +cfQ== 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:in-reply-to :references: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=AIeyZAr2Q8dgdvxDXp519gp0OXgJYNgdTzrV2wN2ZdA=; b=c7VLkmEhI3p0BnZ8r6Bu3wfyvO30xvpZlT+nFsgi6woHf7pJa5Gf3/Wf/2SmAefegV +NweboVLg6IYu86rq/lW/8XsqppGh3mXiLw+EDC/k3BeJCR+iYVv+856UH9FYLzbjsiT 0AVnyMkrV1nYi6Pc1CtIwcl7xxH3xA6Bmqs29gQTN3XuTLZ7y2X0jSrvurtJaTJcZ5V1 qCgzH5+M4ELHOvdWognhSgUm8UOF1NbFzz+InKTPMrVGD5CIM22AN5MDAmv3z30dtlz7 Wk4WTHKQH4KNuwlf7hlLp1TFR6ftEsrdVrxZKuTkE2t7N0mfVefkQtXRprcXnGG3c6PU NGuA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUpyXLK3iPGCmIc9nD4O61j2FpQS6dqrtcvyTShMM0nP9OZm2jT 2g5TnZTONlb5mqUtNJhO9TQ= X-Google-Smtp-Source: APXvYqx1nAnzToikfqyFhAsciEUDysnRsZLXCyQFS2TC7nxkYacCIThwuC+b57ALZIfxS0sK37eoFw== X-Received: by 2002:a9d:6c89:: with SMTP id c9mr31122773otr.52.1559156679817; Wed, 29 May 2019 12:04:39 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:ba2:: with SMTP id 31ls613343oth.2.gmail; Wed, 29 May 2019 12:04:39 -0700 (PDT) X-Received: by 2002:a9d:7092:: with SMTP id l18mr2712256otj.301.1559156679061; Wed, 29 May 2019 12:04:39 -0700 (PDT) Date: Wed, 29 May 2019 12:04:38 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: In-Reply-To: References: <18681ec4-dc8d-42eb-b42b-b9a9f639d89e@googlegroups.com> <3f6331a7-688e-570b-01d8-d02a81eac96b@inria.fr> <9232f85a-6d64-84dc-a2d0-290c0fc6e760@cse.gu.se> Subject: Re: [HoTT] doing "all of pure mathematics" in type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_30_1800501822.1559156678227" X-Original-Sender: escardo.martin@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_30_1800501822.1559156678227 Content-Type: multipart/alternative; boundary="----=_Part_31_1489244913.1559156678227" ------=_Part_31_1489244913.1559156678227 Content-Type: text/plain; charset="UTF-8" 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 such 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/msgid/HomotopyTypeTheory/c7197bc2-7fc5-4027-bed6-24b2d350950f%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_31_1489244913.1559156678227 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
=C2=A0Thanks for this discussion. I like it.=C2=A0

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 o= f the
> truth of *something they already knew*.

=
I am not sure why the person who started this thread, a mathemat= ician,
Kevin Buzzard, decided to put in such a lot of work, but d= id and he
has (in Lean), with his students.

<= div>But having interacted with a lot of students (from my institution, and<= /div>
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 tryi= ng to
convince the computer.=C2=A0

They = are trying to convince themselves, using the computer to both=C2=A0
check their understanding and record their understanding when=C2=A0
the proof is complete.

If I am allowed to sp= eak for myself, I created a univalent library in
Agda for the pur= pose of *doing something else*. However, it is nice to
stare at t= he library and see everything developed from first
principles. Wh= en presented with the mathematical literature, both as
students a= nd experienced mathematicians, we are never sure how far
back one= has to read until everything begins in a precise way. How
much h= ave we created, and how do all the different fields of
mathematic= s interact with each other? When one records mathematics in
the c= omputer, this begins to become clear, or at least the asnwers to such
=
questions become possible.

We don't need = to *convince* anybody. This will *happen*. And it is
already happ= ening. The students like it. This is my experience.

M.


--
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/c7197bc2-7fc5-4027-bed6-24b2d350950f%40googleg= roups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_31_1489244913.1559156678227-- ------=_Part_30_1800501822.1559156678227--