"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:
"We are a group of two dozen mathematicians who wrote a 600 page book in less than half a year. This is quite amazing, since mathematicians do not normally work together in large groups. In a small group they can get away with using obsolete technology, such as sending each other source LaTeX files by email, but with two dozen people even Dropbox or any other file synchronization system would have failed miserably...We used git and github.com. In the beginning it took some convincing and getting used to, although it was not too bad. In the end the repository served not only as an archive for our files, but also as a central hub for planning and discussions. For several months I checked github more often than email and Facbook. Github was my Facebook (without the cute kittens)....
But more importantly, the spirit of collaboration that pervaded our group at the Institute for Advanced Study was truly amazing. We did not fragment. We talked, shared ideas, explained things to each other, and completely forgot who did what (so much in fact that we had to put some effort into reconstruction of history lest it be forgotten forever). The result was a substantial increase in productivity. There is a lesson to be learned here... namely that mathematicians benefit from being a little less possessive about their ideas and results. I know, I know, academic careers depend on proper credit being given and so on, but really those are just the idiosyncrasies of our time. If we can get mathematicians to share half-baked ideas, not to worry who contributed what to a paper, or even who the authors are, then we will reach a new and unimagined level of productivity. Progress is made by those who dare break the rules.
Truly open research habitats cannot be obstructed by copyright, profit-grabbing publishers, patents, commercial secrets, and funding schemes that are based on faulty achievement metrics. Unfortunately we are all caught up in a system which suffers from all of these evils. But we made a small step in the right direction by making the book source code freely available under a permissive Creative Commons license. Anyone can take the book and modify it, send us improvements and corrections, translate it, or even sell it without giving us any money. (If you twitched a little bit when you read that sentence then the system has gotten to you.)
We decided not to publish the book with an academic publisher at present because we wanted to make it available to everyone fast and at no cost. The book can be freely downloaded, as well as bought cheaply in hardcover and paperback versions from lulu.com. (When was the last time you paid under $30 for a 600 page hardcover academic monograph?) Again, I can feel some people thinking “oh but a real academic publisher bestows quality”...Yes, good quality of research must be ensured. But once we accept the fact that anyone can publish anything on the Internet for the whole world to see, and make a cheap professionally looking book out of it, we quickly realize that censure is not effective anymore. Instead we need a decentralized system of endorsments which cannot be manipulated by special interest groups. Things are moving in this direction with the recently established Selected Papers Network and similar efforts. I hope these will catch on.
However, there is something else we can do. It is more radical, but also more useful. Rather than letting people only evaluate papers, why not give them a chance to participate and improve them as well? Put all your papers on github and let others discuss them, open issues, fork them, improve them, and send you corrections. Does it sound crazy? Of course it does, open source also sounded crazy when Richard Stallman announced his manifesto. Let us be honest, who is going to steal your LaTeX source code? There are much more valuable things to be stolen. If you are tenured professor you can afford to lead the way. Have your grad student teach you git and put your stuff somewhere publicly. Do not be afraid, they tenured you to do such things.
So we are inviting everyone to help us improve the book by participating on github. You can leave comments, point out errors, or even better, make corrections yourself! We are not going to worry who you are, how much you are contributing, and who shall take credit. The only thing that matters is whether your contributions are any good.
My last observation is about formalization of mathematics. Mathematicians like to imagine that their papers could in principle be formalized in set theory. This gives them a feeling of security, not unlike the one experienced by a devout man entering a venerable cathedral. It is a form of faith professed by logicians. Homotopy Type Theory is an alternative foundation to set theory."--Andrej Bauer,
Recent Comments