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 >> Bloch-Kato, because he was sure it was right. (I should have asked him at >> the time how he could be so sure!) >> > > Oh this is interesting... do you remember when this conversation was > happening? Because in these slides ( > https://www.math.ias.edu/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’s 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 "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/3811fd43-0b84-4ac0-adcd-de638ae3ad57%40googlegroups.com.