"The usual implicit assumption is that mathematical English could be formalized in a set-theoretic foundation such as ZFC, and this requires various conventions on what we can and can’t say in mathematical English. The goal of informal type theory is to develop conventions for a version of mathematical English whose “implicit underlying foundation” is instead type theory — specifically, homotopy type theory."--Mike Shulman.
"Writing a 500 pp. book on an entirely new subject, with 40 authors, in 9 months is already an amazing achievement....But even more astonishing, in my humble opinion, is the mathematical and logical content: this is an entirely new foundation, starting from scratch and reaching to , the Yoneda lemma, the cumulative hierarchy of sets, and a new constructive treatment of the real numbers — with a whole lot of new and fascinating mathematics and logic along the way...But for all that, what is perhaps most remarkable about the book is what is not in it: formalized mathematics. One of the novel things about HoTT is that it is not just formal logical foundations of mathematics in principle: it really is code that runs in a computer proof assistant... At the risk of sounding a bit grandiose, this represents something of a “new paradigm” for mathematics: fully formal proofs that can be run on the computer to ensure their absolute rigor, accompanied by informal exposition that can focus more on the intuition and examples. Our goal in this Book has been to provide a first, extended example of this new style of doing mathematics."--Steve Awodey.
[HT Choice & Inference] And on the future sociology of mathematics:
Continue reading "Alternative Foundations in the Faith of Mathematics-land" »
Recent Comments