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.9 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-qt1-x83f.google.com (mail-qt1-x83f.google.com [IPv6:2607:f8b0:4864:20::83f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0c9efcac for ; Sun, 3 Nov 2019 11:57:11 +0000 (UTC) Received: by mail-qt1-x83f.google.com with SMTP id g5sf9217821qtc.5 for ; Sun, 03 Nov 2019 03:57:11 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1572782230; cv=pass; d=google.com; s=arc-20160816; b=YNLNV9BTLM/4d/EAr0F1Shcp1+a3tJq69Qi17I5I2IYUiEbe2vE27GpnKY2s0J7e1B ypIjPSYVe56BNAvgIO5VtNpOI9JkJ96aLlWAvvCO/wZzuY6J2PgIohKsMYrD8HLqol6W vHL1niQAVe9AqI7YP/PkG2vIsws8n/tfkPUbZK/QQV7OkST9evTGz80Dub9j+jZ671Uh l9pht9cP+8xxgA1G5R7sD2V8tm7j95c5lZFDZb8kMYzGH79aS4WDpO0Ssg2Xw+1XNdX9 IstqlgNgWg9cRP0Yvcj6vARfkAUf7zDn79m9bb/KvWrS61XxOLSoIwIcvKTAqm2/atFV nPwQ== 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=oimcpISKeSvUGiGGNfuxRSBVmDRylYvylwRjZxGqQCo=; b=IXDeODdLQ4zONWovmzigl7PbRdcwc4MLVrj1B5+p7xbsNvzax6CfiZ4q9YdnzRN7cg Tlw4mBJY6MSKhjGOWgCiGiWQLzy3seOVzZbyWVdYa3xYXS7xYmecemy+pUWrhjEQ+YGl xYue3nNfcVOeoyAXH3zrvLwg9fHgWv3Z6JKM6Yt+KJ8QigZcET2/m2nOUBfg6u6XFZUh F1fL48P45JGVfhCgoZFCuaZubv1Ydt2qfMBRW8OJyWnAnoXseFgb59wvanxfrNplMEvk +GjivbhRK2ETrYrARpJF/wQiPzziTZENP7Q+msghC5PZqMjsJC1MGbwql/0vu3IaEbxq JMgg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=a5lbXmXe; spf=pass (google.com: domain of droberts.65537@gmail.com designates 2607:f8b0:4864:20::b32 as permitted sender) smtp.mailfrom=droberts.65537@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=oimcpISKeSvUGiGGNfuxRSBVmDRylYvylwRjZxGqQCo=; b=RIB9BSYkyfTGv1xZVGuFHVjq+ORZw42p0+ekQn+jYKmAr342WNEO+ymmCtauD2zJBu P1yb/GPrsS9rveOGnZZz+U6HtN2e9bGd2O/zZkNz5ScqQFGpBFkW+DfVbsLeZguKlHIG ivv+aYiYBWCgSTP7fksjy4QYuvztEjFRrwykd2FU4hK6O6Ww6iUpm1ecjYI5GeBw6Frl RyPDH5QsM2MIBs8/fBTYXxJepFuHnkcLetia7qs+lALvjSPh2fdGjzjbjN+/ijXSqExN psRBxjYmXN8ZrLBP6XI4M/yKd4V6xOMCDy3NQDO907Y2hZb3V/Z2B/e20iPIq75X4tSO Az7w== 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=oimcpISKeSvUGiGGNfuxRSBVmDRylYvylwRjZxGqQCo=; b=N3PyIW27QTpx7zKc3+Pqm79YrsZs8v0UOMYxlogwEu0A5FhLDPvsE86jkO7cnrD3RV dIeAesnWNb5wcD4av9Qlp3XFH71MU2f1Ze7mgG6KueHxhL9PlZI5dgeBJFX5LY1iFuAo MrlpCBNVmQ/9cUg9R2T+WWI1EEmsZtOpkMGDRKDM4ZR43zpo33XhOZBcxD5Hvyu9v9/b GSshgTf+Zc6EKP41Wxb6g5SPyA9QWwuqgx12CbjExiRaaNOMVCfwBJdWQrtrbkS1pPtf v+c+iRq7UrB6OaiyDCh5fwdckSeX+iP9bMHDdEJ5wFrIUNpO+MnnR+hhFeqOVVp5RVOr y/Gw== 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=oimcpISKeSvUGiGGNfuxRSBVmDRylYvylwRjZxGqQCo=; b=HSoljVLBQny31bVn1iQur0VJZGQb/acNS/nUzLEsZyGSPGkzW1k22XzbG4Xdk7P2Yr L8x64+Zaqg715fpsHp96HV3ysj8+pp2UjCMM8N/r3AzQdeKyQHXe0qmICDyD15SIjSJq 2pGWlxcVILX+WpAs/lDwaZp2lR2PDkNPjbs8mBp24MNC3YMvg3yLP41ltfiiGp5nIntY +bSRiJntmr9ejwzrJEi+UcQvKaWzrXYxYT55FMp8dSQTNdM3OhYQJoDo/UBITt9j01Sv EI6CDXf4kOfuF3h6tH2qEvUWlzyM0jqp8m0gz9kTjDwEepvW5QOcRt7fhzcip+gqgGZP BXIA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVsSY7K97OZ6EZd7jbkEfLnG/ec1WdY7zFep3blZzQzLu8PgNNo LURUN/Bft0RCtD1/5BLdfW0= X-Google-Smtp-Source: APXvYqyfOvcxMJPqJgVJLO5UZ6z9DjQanZmNCHFrXaY1ldhi/EEFOe6yMpaREJ0CFnJvuyWb8TSH1Q== X-Received: by 2002:a05:620a:634:: with SMTP id 20mr13464634qkv.330.1572782230228; Sun, 03 Nov 2019 03:57:10 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:d6d0:: with SMTP id l16ls2019175qvi.1.gmail; Sun, 03 Nov 2019 03:57:09 -0800 (PST) X-Received: by 2002:a0c:f987:: with SMTP id t7mr1915832qvn.133.1572782229809; Sun, 03 Nov 2019 03:57:09 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1572782229; cv=none; d=google.com; s=arc-20160816; b=1CSGQ7kWbPoFP66BNL11U7H2DQEgJCz0c5FyWpahM4Lh++abJiTtXvk9jptU46vqIY m3mKcPlsrqaO6toHq0YD3KmdRkXAi9WAzEHt+cOt+MzT74bxAJG3z6C10k9qSKzDu3IH mVABe/F1+xfeY7DtI9o/KcCDWlVr2dGTJUdbHAKNZ2HSrv/FPK099HkMNejTh6VsgMYS Un8y6kaJayI3sYNy2mSndQ2kwgZa+/xgOdyxPjOo30Vfq++jQNdD6GEzNqZ34fzvEb4l o1N4qvFiecC0kfQxqYZJ1DWFXevWWQDbc/+gR/ujwe9ZniV9DSKsHzun0+cB7Mv1UUbb xVIA== 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=9NhDxwVuygtEZewE1fqbVl+cdlPX+7l0dNWxCgOv0MA=; b=V+jlQgggnJjHk0zqWglM9moBKZiJRFCYyY5ZS7cfU6tpVr8j6X5g5RctY6VNwAnhrx B9GJnDjBAhl3ebKHCA+ATP/K0Dz126anBHxDzQxPox5PJm+FKOtHnDYikTV7yyHhWcUw xmFVEYkQM+7BZqXoa5cnPfDPshw/ATz8hjWhRiH8ubHfQ4XBgoLOhnsTOIlUm7xCmEAQ sYu8bcQ43CXtGjuwVdewqQAYAZ62Bns9j/M8VqLb1HrAYO0eQT/hK/1FSbFDArXmAIZu ZFcn+j1wlQF0AKd+ZuLau9Va47N9xkdLzKK2vaOHdU4IGNlObTIcxXZB1RoMu201jXNy vh9w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=a5lbXmXe; spf=pass (google.com: domain of droberts.65537@gmail.com designates 2607:f8b0:4864:20::b32 as permitted sender) smtp.mailfrom=droberts.65537@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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 w140si852798qka.6.2019.11.03.03.57.09 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 03 Nov 2019 03:57:09 -0800 (PST) Received-SPF: pass (google.com: domain of droberts.65537@gmail.com 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 i12so547163ybg.2 for ; Sun, 03 Nov 2019 03:57:09 -0800 (PST) X-Received: by 2002:a25:7187:: with SMTP id m129mr19557045ybc.236.1572782229432; Sun, 03 Nov 2019 03:57:09 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: David Roberts Date: Sun, 3 Nov 2019 22:22:04 +1030 Message-ID: Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? To: Bas Spitters , homotopytypetheory Cc: Nicolas Alexander Schmidt Content-Type: multipart/alternative; boundary="0000000000001832ff05966fe603" X-Original-Sender: droberts.65537@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=a5lbXmXe; spf=pass (google.com: domain of droberts.65537@gmail.com designates 2607:f8b0:4864:20::b32 as permitted sender) smtp.mailfrom=droberts.65537@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: , --0000000000001832ff05966fe603 Content-Type: text/plain; charset="UTF-8" Forget even higher category theory. Kevin Buzzard now goes around telling the story of how even formally proving (using Lean) things in rather elementary commutative algebra from EGA that are stated as equalities was not obvious: the equality is really an isomorphism arising from a universal property. Forget trying to do anything motivic, when algebra is full of such equalities. This is not a problem with univalence, of course. David On Sun, 3 Nov 2019, 10:08 PM Bas Spitters wrote: > There's also VV homotopy lambda calculus, which he later abandoned for > MLTT: > > https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf > > On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters > wrote: > >> I believe it refers to his 2-theories: >> https://www.ias.edu/ideas/2014/voevodsky-origins >> >> On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt < >> zero@fromzerotoinfinity.xyz> wrote: >> >>> In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 talk >>> at IAS, Voevodsky talks about the history of his project of "univalent >>> mathematics" and his motivation for starting it. Namely, he mentions >>> that he found existing proof assistants at that time (in 2000) to be >>> impractical for the kinds of mathematics he was interested in. >>> >>> Unfortunately, he doesn't go into details of what mathematics he was >>> exactly interested in (I'm guessing something to do with homotopy >>> theory) or why exactly existing proof assistants weren't practical for >>> formalizing them. Judging by the things he mentions in his talk, it >>> seems that (roughly) his rejection of those proof assistants was based >>> on the view that predicate logic + ZFC is not expressive enough. In >>> other words, there is too much lossy encoding needed in order to >>> translate from the platonic world of mathematical ideas to this formal >>> language. >>> >>> Comparing the situation to computer programming languages, one might say >>> that predicate logic is like Assembly in that even though everything can >>> be encoded in that language, it is not expressive enough to directly >>> talk about higher level concepts, diminishing its practical value for >>> reasoning about mathematics. In particular, those systems are not >>> adequate for *interactive* development of *new* mathematics (as opposed >>> to formalization of existing theories). >>> >>> Perhaps I am just misinterpreting what Voevodsky said. In this case, I >>> hope someone can correct me. However even if this wasn't *his* view, to >>> me it seems to be a view held implicitly in the HoTT community. In any >>> case, it's a view that one might reasonably hold. >>> >>> However I wonder how reasonable that view actually is, i.e. whether e.g. >>> Mizar really is that much more impractical than HoTT-Coq or Agda, given >>> that people have been happily formalizing mathematics in it for 46 years >>> now. And, even though by browsing the contents of "Formalized >>> Mathematics" one can get the impression that the work consists mostly of >>> formalizing early 20th century mathematics, neither the UniMath nor the >>> HoTT library for example contain a proof of Fubini's theorem. >>> >>> So, to put this into one concrete question, how (if at all) is HoTT-Coq >>> more practical than Mizar for the purpose of formalizing mathematics, >>> outside the specific realm of synthetic homotopy theory? >>> >>> >>> -- >>> >>> 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/e491d38b-b50a-6172-dca9-40d45fe1b6d2%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/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com > > . > -- 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/CAFL%2BZM_%3D%3DiLS16Vy7sGiEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.com. --0000000000001832ff05966fe603 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Forget even higher category theory. Kevin Buzzard now goe= s around telling the story of how even formally proving=C2=A0(using Lean)=C2=A0things in rather elementa= ry commutative algebra from EGA that are stated as equalities was not obvio= us: the equality is really an isomorphism arising from a universal property= . Forget trying to do anything motivic, when algebra is full of such equali= ties. This is not a problem with univalence, of course.
David

<= div dir=3D"ltr" class=3D"gmail_attr">On Sun, 3 Nov 2019, 10:08 PM Bas Spitt= ers <b.a.w.spitters@gmail.co= m> wrote:
<= div>There's also VV homotopy lambda calculus, which he later abandoned = for MLTT:

On Sun, Oct 27, 2019 at 6:22 P= M Bas Spitters <b.a.w.spitters@gmail.com> wrote:
<= blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-l= eft:1px solid rgb(204,204,204);padding-left:1ex">
I be= lieve it refers to his 2-theories:

On Sun, Oct 27, 2019= at 3:41 PM Nicolas Alexander Schmidt <zero@fromzerotoinfinity.= xyz> wrote:
In [this](https://www.youtub= e.com/watch?v=3Dzw6NcwME7yI&t=3D1680) 2014 talk
at IAS, Voevodsky talks about the history of his project of "univalent=
mathematics" and his motivation for starting it. Namely, he mentions that he found existing proof assistants at that time (in 2000) to be
impractical for the kinds of mathematics he was interested in.

Unfortunately, he doesn't go into details of what mathematics he was exactly interested in (I'm guessing something to do with homotopy
theory) or why exactly existing proof assistants weren't practical for<= br> formalizing them. Judging by the things he mentions in his talk, it
seems that (roughly) his rejection of those proof assistants was based
on the view that predicate logic + ZFC is not expressive enough. In
other words, there is too much lossy encoding needed in order to
translate from the platonic world of mathematical ideas to this formal
language.

Comparing the situation to computer programming languages, one might say that predicate logic is like Assembly in that even though everything can be encoded in that language, it is not expressive enough to directly
talk about higher level concepts, diminishing its practical value for
reasoning about mathematics. In particular, those systems are not
adequate for *interactive* development of *new* mathematics (as opposed
to formalization of existing theories).

Perhaps I am just misinterpreting what Voevodsky said. In this case, I
hope someone can correct me. However even if this wasn't *his* view, to=
me it seems to be a view held implicitly in the HoTT community. In any
case, it's a view that one might reasonably hold.

However I wonder how reasonable that view actually is, i.e. whether e.g. Mizar really is that much more impractical than HoTT-Coq or Agda, given
that people have been happily formalizing mathematics in it for 46 years now. And, even though by browsing the contents of "Formalized
Mathematics" one can get the impression that the work consists mostly = of
formalizing early 20th century mathematics, neither the UniMath nor the
HoTT library for example contain a proof of Fubini's theorem.

So, to put this into one concrete question, how (if at all) is HoTT-Coq
more practical than Mizar for the purpose of formalizing mathematics,
outside the specific realm of synthetic homotopy theory?


--

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@googl= egroups.com.
To view this discussion on the web visit https://g= roups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe= 1b6d2%40fromzerotoinfinity.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@googleg= roups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/Homotop= yTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.= gmail.com.

--
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 htt= ps://groups.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM_%3D%3DiLS16Vy7s= GiEqNkCxOMYL4j%2BZFqKv5uJ-ivkuemEg%40mail.gmail.com.
--0000000000001832ff05966fe603--