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-oi1-x237.google.com (mail-oi1-x237.google.com [IPv6:2607:f8b0:4864:20::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id cfa8a399 for ; Tue, 5 Nov 2019 20:29:59 +0000 (UTC) Received: by mail-oi1-x237.google.com with SMTP id j14sf7934126oie.1 for ; Tue, 05 Nov 2019 12:29:58 -0800 (PST) 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=Isn/VK0U11Vi+j59RbIppCrc5cTDJ5nDQ+hBlzA68IQ=; b=YIViIZI7epnvOiCSF4/gaP72/BLxGc7FdYpztFF6vWJZCr8i1kNaSkRcwMRC/D0a+d GwaCG820KotBx5i2EJjfXBmUvCe/3qaTuBw6A8Uu262RYZLOPa56G1YcmomEZxxzBy59 oitEOrfCvVk7sCOtUQN+NWTmRK3QfDtL3UKLAgtDkTq66kLD0z1HrBik7YDI191GLsqZ w3c7yW8DgDX7tZbKUtDI3PO7QU06S/kP4WfpALApDzgpQt3+OirLgRzpmG2xXpu54195 R35F86+O+vxkOiJSq0tSWjdaVXs/OgZD5UgjencbHSloqt2/90BhG1KtLeHy8c2KxYdJ oRyg== 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=Isn/VK0U11Vi+j59RbIppCrc5cTDJ5nDQ+hBlzA68IQ=; b=mdRNiKhlL3vggqiMhzwSCjZt/hMItAWCjOK2sql2UNQ16lgv14zIpE1SczNZh7YY2+ YpDoG/RbhyR8258daJb47wNPpWRD910oNsl2mGntuD4fSIKSHyAgd0jfPDiX/YrwA2OX wxgBpBJg92paTJpWTdfOwlET7n5BhTfCxgxcwnolMpbmSsw90lsCnwUAcn9IFsb0iv61 tHk5Iu4E/5sFIaZqYdm15MhIJxo7DHawP0nvInX68r6EyHeSZJYOPNcNS9QoV6LnfMQu C8dONFEyi5hwYzU1UUT6XyP3zqTbly9j4jB1iamgIRPh/eWgt3i8KU7IYL0txO3Sglgp rX8g== 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=Isn/VK0U11Vi+j59RbIppCrc5cTDJ5nDQ+hBlzA68IQ=; b=SssJBVVodatGWeTHneOe612XJeAd+GA19t4Wom101W1ilOXXGhP1R8bNNWkvm1Zd65 evrA3de8OqifswCi0Zuu8EA/BLaTPRZ9n+OspdPSHdR8kXUGa9v4R4Wb5+DeuGcRTZX1 d7a2dPeu0akV/Lx8nVBNE3jQwjBU27Hj9I4vwtdOsm4wP5lgtBmfFmwaVCp17kA4kogk P2sXZzqXJLIMGNwywoboW61xECgS62fh9A68INSDSMc+p9SPiXpkQIz9uIFMf2JoS0MA qMcr+ewdq4Q1njX9KnX3wH25ab5ayBIvGQW46VjBAAQOjV6rsosJcu6od5a7+wZb7yY1 avjw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWfpqy2+ED/xrhuI/wx64opRvi5tmAIoS5wa5qRM6h5Rn/mJlZS eRcKo8pteqXnPnIZXI6hvLs= X-Google-Smtp-Source: APXvYqzkrc+mTxabqRaAmpFwGlLW1chvo0Sj+G78cBCKx/PrDVNyxG564FIiAH8mN2FPg5TCuNjgFQ== X-Received: by 2002:a05:6830:1609:: with SMTP id g9mr1556203otr.152.1572985797853; Tue, 05 Nov 2019 12:29:57 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:66d8:: with SMTP id t24ls4389otm.3.gmail; Tue, 05 Nov 2019 12:29:57 -0800 (PST) X-Received: by 2002:a9d:634f:: with SMTP id y15mr24602247otk.5.1572985797290; Tue, 05 Nov 2019 12:29:57 -0800 (PST) Date: Tue, 5 Nov 2019 12:29:56 -0800 (PST) From: Yuhao Huang To: Homotopy Type Theory Message-Id: <0ef61665-eafd-40a0-8592-11bdd277d10b@googlegroups.com> In-Reply-To: References: Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1993_1848494097.1572985796313" X-Original-Sender: temp.use88@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_1993_1848494097.1572985796313 Content-Type: multipart/alternative; boundary="----=_Part_1994_144301713.1572985796313" ------=_Part_1994_144301713.1572985796313 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > > He once told me that he wasn't interested in formalizing his proof of=20 > Bloch-Kato, because he was sure it was right. (I should have asked him a= t=20 > the time how he could be so sure!) > Oh this is interesting... do you remember when this conversation was=20 happening? Because in these slides ( https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_09= _Bernays_3%20presentation.pdf)=20 he said "Next year I am starting a project of univalent formalization of my= =20 proof of Milnor=E2=80=99s Conjecture using this formalization of set theory= as the=20 starting point." (Page 11) =E5=9C=A8 2019=E5=B9=B411=E6=9C=885=E6=97=A5=E6=98=9F=E6=9C=9F=E4=BA=8C UTC= -8=E4=B8=8A=E5=8D=887:43:06=EF=BC=8CDaniel R. Grayson=E5=86=99=E9=81=93=EF= =BC=9A > > Re: "To get back to the original question, my understanding was that=20 > Voevodsky had done a bunch of scheme theory and it had got him a Fields= =20 > medal and it was this mathematics which he was interested in at the time.= =20 > He wanted to formalise his big theorem, just like Hales did." > > I think he was more interested in formalizing things like his early work= =20 > with Kapranov on higher categories, which turned out to have a mistake in= =20 > it. He once told me that he wasn't interested in formalizing his proof o= f=20 > Bloch-Kato, because he was sure it was right. (I should have asked him a= t=20 > the time how he could be so sure!) > > Re: "The clearest evidence, in my mind, is that there is no definition of= =20 > a scheme in UniMath." > > That's sort of accidental. In early 2014, expecting to speak at an=20 > algebraic geometry in the summer, he mentioned that one idea he had for h= is=20 > talk would be to formalize the definition of scheme in UniMath and speak= =20 > about it. I think he was distracted from that by thinking about=20 > C-systems. The UniMath project aims at formalizing all of mathematics, s= o=20 > the definition of scheme is one of the next things that (still) needs to = be=20 > done. > =E5=9C=A8 2019=E5=B9=B411=E6=9C=885=E6=97=A5=E6=98=9F=E6=9C=9F=E4=BA=8C UTC= -8=E4=B8=8A=E5=8D=887:43:06=EF=BC=8CDaniel R. Grayson=E5=86=99=E9=81=93=EF= =BC=9A > > Re: "To get back to the original question, my understanding was that=20 > Voevodsky had done a bunch of scheme theory and it had got him a Fields= =20 > medal and it was this mathematics which he was interested in at the time.= =20 > He wanted to formalise his big theorem, just like Hales did." > > I think he was more interested in formalizing things like his early work= =20 > with Kapranov on higher categories, which turned out to have a mistake in= =20 > it. He once told me that he wasn't interested in formalizing his proof o= f=20 > Bloch-Kato, because he was sure it was right. (I should have asked him a= t=20 > the time how he could be so sure!) > > Re: "The clearest evidence, in my mind, is that there is no definition of= =20 > a scheme in UniMath." > > That's sort of accidental. In early 2014, expecting to speak at an=20 > algebraic geometry in the summer, he mentioned that one idea he had for h= is=20 > talk would be to formalize the definition of scheme in UniMath and speak= =20 > about it. I think he was distracted from that by thinking about=20 > C-systems. The UniMath project aims at formalizing all of mathematics, s= o=20 > the definition of scheme is one of the next things that (still) needs to = be=20 > done. > =E5=9C=A8 2019=E5=B9=B411=E6=9C=885=E6=97=A5=E6=98=9F=E6=9C=9F=E4=BA=8C UTC= -8=E4=B8=8A=E5=8D=887:43:06=EF=BC=8CDaniel R. Grayson=E5=86=99=E9=81=93=EF= =BC=9A > > Re: "To get back to the original question, my understanding was that=20 > Voevodsky had done a bunch of scheme theory and it had got him a Fields= =20 > medal and it was this mathematics which he was interested in at the time.= =20 > He wanted to formalise his big theorem, just like Hales did." > > I think he was more interested in formalizing things like his early work= =20 > with Kapranov on higher categories, which turned out to have a mistake in= =20 > it. He once told me that he wasn't interested in formalizing his proof o= f=20 > Bloch-Kato, because he was sure it was right. (I should have asked him a= t=20 > the time how he could be so sure!) > > Re: "The clearest evidence, in my mind, is that there is no definition of= =20 > a scheme in UniMath." > > That's sort of accidental. In early 2014, expecting to speak at an=20 > algebraic geometry in the summer, he mentioned that one idea he had for h= is=20 > talk would be to formalize the definition of scheme in UniMath and speak= =20 > about it. I think he was distracted from that by thinking about=20 > C-systems. The UniMath project aims at formalizing all of mathematics, s= o=20 > the definition of scheme is one of the next things that (still) needs to = be=20 > done. > --=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/0ef61665-eafd-40a0-8592-11bdd277d10b%40googlegroups.com. ------=_Part_1994_144301713.1572985796313 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
= He once told me that he wasn't interested in formalizing his proof of= =20 Bloch-Kato, because he was sure it was right.=C2=A0 (I should have asked hi= m=20 at the time how he could be so sure!)

O= h this is interesting... do you remember when this conversation was happeni= ng? Because in these slides (http= s://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2014_09_Ber= nays_3%20presentation.pdf) he said "Next year I am starting a proj= ect of univalent formalization of my proof of Milnor=E2=80=99s Conjecture u= sing this formalization of set theory as the starting point." (Page 11= )

=E5=9C=A8 2019=E5=B9=B411=E6=9C=885=E6=97=A5=E6= =98=9F=E6=9C=9F=E4=BA=8C UTC-8=E4=B8=8A=E5=8D=887:43:06=EF=BC=8CDaniel R. G= rayson=E5=86=99=E9=81=93=EF=BC=9A
Re: "To get back to the original question, my unde= rstanding was that Voevodsky had done a bunch of scheme theory and it had g= ot him a Fields medal and it was this mathematics which he was interested i= n at the time. He wanted to formalise his big theorem, just like Hales did.= "

I think he was more interested in formalizing= things like his early work with Kapranov on higher categories, which turne= d out to have a mistake in it.=C2=A0 He once told me that he wasn't int= erested in formalizing his proof of Bloch-Kato, because he was sure it was = right.=C2=A0 (I should have asked him at the time how he could be so sure!)=

Re: "The clearest evidence, in my mind, is that there is no de= finition of a scheme in UniMath."

That's sort of accidental= .=C2=A0 =C2=A0In early 2014, expecting to speak at an algebraic geometry in= the summer, he mentioned that one idea he had for his talk would be to for= malize the definition of scheme in UniMath and speak about it.=C2=A0 I thin= k he was distracted from that by thinking about C-systems.=C2=A0 The UniMat= h project aims at formalizing all of mathematics, so the definition of sche= me is one of the next things that (still) needs to be done.

=E5=9C=A8 2019=E5=B9=B411=E6=9C=885=E6=97=A5=E6=98=9F=E6=9C=9F= =E4=BA=8C UTC-8=E4=B8=8A=E5=8D=887:43:06=EF=BC=8CDaniel R. Grayson=E5=86=99= =E9=81=93=EF=BC=9A
Re: "To get back to the original question, my understanding was t= hat Voevodsky had done a bunch of scheme theory and it had got him a Fields= medal and it was this mathematics which he was interested in at the time. = He wanted to formalise his big theorem, just like Hales did."
=
I think he was more interested in formalizing things like hi= s early work with Kapranov on higher categories, which turned out to have a= mistake in it.=C2=A0 He once told me that he wasn't interested in form= alizing his proof of Bloch-Kato, because he was sure it was right.=C2=A0 (I= should have asked him at the time how he could be so sure!)

Re: &qu= ot;The clearest evidence, in my mind, is that there is no definition of a s= cheme in UniMath."

That's sort of accidental.=C2=A0 =C2=A0I= n early 2014, expecting to speak at an algebraic geometry in the summer, he= mentioned that one idea he had for his talk would be to formalize the defi= nition of scheme in UniMath and speak about it.=C2=A0 I think he was distra= cted from that by thinking about C-systems.=C2=A0 The UniMath project aims = at formalizing all of mathematics, so the definition of scheme is one of th= e next things that (still) needs to be done.

= =E5=9C=A8 2019=E5=B9=B411=E6=9C=885=E6=97=A5=E6=98=9F=E6=9C=9F=E4=BA=8C UTC= -8=E4=B8=8A=E5=8D=887:43:06=EF=BC=8CDaniel R. Grayson=E5=86=99=E9=81=93=EF= =BC=9A
Re: &qu= ot;To get back to the original question, my understanding was that Voevodsk= y had done a bunch of scheme theory and it had got him a Fields medal and i= t was this mathematics which he was interested in at the time. He wanted to= formalise his big theorem, just like Hales did."

I think he was more interested in formalizing things like his early work= with Kapranov on higher categories, which turned out to have a mistake in = it.=C2=A0 He once told me that he wasn't interested in formalizing his = proof of Bloch-Kato, because he was sure it was right.=C2=A0 (I should have= asked him at the time how he could be so sure!)

Re: "The clear= est evidence, in my mind, is that there is no definition of a scheme in Uni= Math."

That's sort of accidental.=C2=A0 =C2=A0In early 2014= , expecting to speak at an algebraic geometry in the summer, he mentioned t= hat one idea he had for his talk would be to formalize the definition of sc= heme in UniMath and speak about it.=C2=A0 I think he was distracted from th= at by thinking about C-systems.=C2=A0 The UniMath project aims at formalizi= ng all of mathematics, so the definition of scheme is one of the next thing= s that (still) needs to be done.

--
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/0ef61665-eafd-40a0-8592-11bdd277d10b%40googleg= roups.com.
------=_Part_1994_144301713.1572985796313-- ------=_Part_1993_1848494097.1572985796313--