Re:How Math’s Most Famous Proof Nearly Broke (2015)
by jeff76 on Friday December 21, 2018 @08:01AM
(#18733038)
This is interesting. What are the prerequisites to understand Univalent Foundations and how active is it?
Re:How Math’s Most Famous Proof Nearly Broke (2015)
by bbeonx on Friday December 21, 2018 @08:12AM
(#18733062)
Look into the Coq language, it is under active development and there is a lot of work going into it. Voevodsky was working in Coq, if I recall.
As to how hard it is to learn, you will have to learn a pretty decent amount. It all depends on your background. If you know what the Curry Howard correspondence is, you are in relatively good shape. If you've never heard of lambda calculus or first order logic, you may have some more work cut out for you.
Here is a nice article I read last night on explaining the move from set theory to type theory. It gets a bit technical but you might be able to get something from it.
https://golem.ph.utexas.edu/category/2013/01/from_set_theory...
Re:How Math’s Most Famous Proof Nearly Broke (2015)
by alimw on Friday December 21, 2018 @01:12PM
(#18735203)
If you're specifically interested in Univalent Foundations, just read the book.
https://homotopytypetheory.org/book/
"Only then did I discover that the proof of a key lemma in my paper contained a mistake and that the lemma, as stated, could not be salvaged. Fortunately, I was able to prove a weaker and more complicated lemma, which turned out to be sufficient for all applications. A corrected sequence of arguments was published in 2006.
This story got me scared. Starting from 1993, multiple groups of mathematicians studied my paper at seminars and used it in their work and none of them noticed the mistake. And it clearly was not an accident."
More details on page 8 in the IAS newsletter article
https://www.ias.edu/sites/default/files/pdfs/publications/le...
There is also a Quanta article:
https://www.quantamagazine.org/univalent-foundations-redefin...