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-x23f.google.com (mail-oi1-x23f.google.com [IPv6:2607:f8b0:4864:20::23f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b86e86cd for ; Wed, 6 Nov 2019 23:59:32 +0000 (UTC) Received: by mail-oi1-x23f.google.com with SMTP id q82sf560045oih.14 for ; Wed, 06 Nov 2019 15:59:31 -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=KVUXylD7awVFSBe+CXa4wYmrY30PXhrGVCFV3j2H1rc=; b=oA5MJ8og8gCN4Bof7n0ziJMpQRonSITecRk+EEPgc+OODwDRVb2MEtdxV6tVjcpDJa JlLLaIIcCr3OQo4wFEjZ3RCIA8JWXddY7bxfGh8/jvD1IRnbrP98VrkMEH/1ur9e5aON zKdPISpTtpeaPexNHb2p5+8HBtLUex/gQR4nEcfylCXd98BRUpvYB8Z64pgN2lt50CuF zZElBx4/WNB+Hn2hU5UEK09DsNRbt2c7t3zJ3mR2bqg4qt6ppoLPu9WsF7KkLNH9oWXU WfsUzn+NvwlXLqs4JRZLgbyVYb8pskeecGRyTReZ4jH3PyhjispMaBZhbGXMboCLqfM+ WWiw== 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=KVUXylD7awVFSBe+CXa4wYmrY30PXhrGVCFV3j2H1rc=; b=jd9aHLqiLIg2b8SQQqkvbpnv7JwC1BBi0/QMWrwlmAETTglZASdcXesVGSRRXxRas6 eYwvbH+ZnWoW24GDvIo0s2WfbR2kAmKsB8/bst5GF85pyeJufqjtI3YJ69H+HLdDLWP5 VNcQ8ZWgvoJJGn8rzDLBhHCteZGOw20yKQ4KF0otFsF9Kn2CgOTh5nJ3vonvlDTstWCK 713ihPQeYRN+UckcQivIu3ZHFjNQXBaZOts0yWxWxhzygoeoMPFAi/h9EsYQ6up3kR/B lNxithZJZQqpuATLt+JmQeUEYD7OmU9mEb3fSdlqBxQv0Kh5XdTHhfTkFK3UqkQiUCIn GQAw== 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=KVUXylD7awVFSBe+CXa4wYmrY30PXhrGVCFV3j2H1rc=; b=Fcnlaf6c5zemPw44SoIPxer+6JDYvhVDgRl2xNbkSH2CbxzQoS8KRomOBp5J/XsC2W kpgsCx14qpF91gFONbCRzBIttR8Qy3ASMetmHt1imF8OwRtukoxOC829NJAHgjpTK663 wzryMW+6D4orr8jkACX5pCMAflLdGiNC1ey7NzvgfaYxcpsMs0TKHA05Mykj3Gn+ubWE 25Z3umolhOKjIp8oTXWbA2eQ7dUGXHLhMqa14taAX1Q3ATDyA7uapndK/I3PYnL2ZX9C kQCXYIaKWs21LJm1GkmGA7Kf696uQj94flTpcS5UtMEgZLsk4sOWpgyrDH5q2+p1alss QPvA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVck/49+bIi0rvCw5Iq9dc2eSM77epl1Fz1Md4NYGN3l6xFQLUd DNetvOl1D21jcb1dyzSKLNg= X-Google-Smtp-Source: APXvYqy8glV+eZyscZhR+6LCUPdzg5Be6M582OXAE9AX23mQNq0TpWSbP0eHHT/7Wiiiu4fMkub8bQ== X-Received: by 2002:a9d:854:: with SMTP id 78mr364411oty.284.1573084770054; Wed, 06 Nov 2019 15:59:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:d1a:: with SMTP id 26ls278425oin.7.gmail; Wed, 06 Nov 2019 15:59:29 -0800 (PST) X-Received: by 2002:aca:280a:: with SMTP id 10mr575066oix.119.1573084769398; Wed, 06 Nov 2019 15:59:29 -0800 (PST) Date: Wed, 6 Nov 2019 15:59:28 -0800 (PST) From: "Daniel R. Grayson" To: Homotopy Type Theory Message-Id: <3811fd43-0b84-4ac0-adcd-de638ae3ad57@googlegroups.com> In-Reply-To: <0ef61665-eafd-40a0-8592-11bdd277d10b@googlegroups.com> References: <0ef61665-eafd-40a0-8592-11bdd277d10b@googlegroups.com> Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2590_388340405.1573084768532" X-Original-Sender: danielrichardgrayson@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_2590_388340405.1573084768532 Content-Type: multipart/alternative; boundary="----=_Part_2591_771639925.1573084768533" ------=_Part_2591_771639925.1573084768533 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Sorry, at this point I don't remember precisely. On Tuesday, November 5, 2019 at 2:29:56 PM UTC-6, Yuhao Huang wrote: > > 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 = at=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 theo= ry as the=20 > starting point." (Page 11) > --=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/3811fd43-0b84-4ac0-adcd-de638ae3ad57%40googlegroups.com. ------=_Part_2591_771639925.1573084768533 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Sorry, at this point I don't remember precisely.
On Tuesday, November 5, 2019 at 2:29:56 PM UTC-6, Yuhao Huang wrote:
He once told me that he wasn't interes= ted 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 (https://www.math.ias.ed= u/vladimir/sites/math.ias.edu.vladimir/files/2014_09_Bernays= _3%20presentation.pdf) he said "Next year I am starting a project = of univalent formalization of my proof of Milnor=E2=80=99s Conjecture using= this formalization of set theory as the starting point." (Page 11)

--
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/3811fd43-0b84-4ac0-adcd-de638ae3ad57%40googleg= roups.com.
------=_Part_2591_771639925.1573084768533-- ------=_Part_2590_388340405.1573084768532--