Public

**A foundations of mathematics for the 21st century**

It's here! For decades, mathematicians been dreaming of an approach to math where different proofs that x = y can be seen as different

*paths*in a

*space*. It's finally been made precise, thanks to Vladimir Voevodsky and a gang of mathematicians who holed up for a year at the Institute for Advanced Studies, at Princeton.

I won't try to explain it, since that's what the book does. I'll just mention a few of the radical new features:

• It includes set theory as a special case, but it's founded on more general things called 'types'. Types include sets, but also propositions. Proving a proposition amounts to constructing an element of a certain type. So, proofs are no longer 'outside' the mathematics being discussed, they're inside it just like everything else.

• The logic is - in general - 'constructive', meaning that to prove something exists amounts to giving a procedure for constructing it. As a result, the system can be

*and is being*computerized with the help of programs like Coq and AGDA.

• Types can be seen as 'spaces', and their elements as 'points'. A proof that two elements of a type are equal can be seen as constructing a path between two points. Sets are just a special case: the '0-types', which have no interesting higher-dimensional aspect. There are also types that look like spheres and tori! Technically speaking, the branch of topology called

*homotopy theory*is now a part of logic! That's why the subject is called

**homotopy type theory**.

• Types can also be seen as

**infinity-groupoids**. Very roughly, these are structures with elements, isomorphisms between elements, isomorphisms between isomorphisms, and so on

*ad infinitum*. So, a certain chunk of the important new branch of math called 'higher category theory' is now part of logic, too.

• The most special contribution of Voevodsky is the

**univalence axiom**. Very

*very*roughly, this expands the concept of 'equality' so that it's just as general as the hitherto more flexible concept of 'isomorphism' - or, if you know some more fancy math, 'equivalence'. Mathematicians working on homotopy theory and higher category theory have known for decades that equality is too rigid a concept to be right - for certain applications. The univalence axiom updates our concept of equality so that it's good again! (However, nobody knows if this axiom is constructive - this is a big open question.)

Since this is all about

*foundations*, and it's all quite new, please don't ask me yet what its practical applications are. Ask me in a hundred years. For now, I can tell you that this is the 'upgrade' that the foundations of math has needed ever since the work of Grothendieck. It's truly 21-century math.

It's also a book for the 21st century, because it's escaped the grip of expensive publishers! While it's 600 pages long, a hardback copy costs less than $27. Paperback costs less than $18, and an electronic copy is free!

#spnetwork #homotopytheory #ncategories #logic #foundations

View 36 previous comments

- New Scientist now has an article on this [ http://www.newscientist.com/article/dn23749-mathematicians-think-like-machines-for-perfect-proofs.html ]Jun 26, 2013
- Thanks, +Kam-Yung Soh! The article mostly misses the point of homotopy type theory, but that's typical of
*New Scientist*, and "all publicity is good publicity".Jun 28, 2013 - Is anything actually incorrect abouy the New Scientist article?

( Even if they missed the immediate point how this breakthrough impacts mathmatics beyond computable proofs ? )Jun 29, 2013 - My complaint about the
*New Scientist*article is not exactly that it has factual errors, but that it mostly misses the point of this new book. Type theory is old news, and so are computer-assisted proofs, and using type theory for computer-assisted proofs. What's new about this book is that it's about**homotopy**type theory. I tried to explain what that means in my post here. The*New Scientist*article doesn't say a word about that.

This*New Scientist*article would have made more sense if it were about the computer-assisted proof of the Feit-Thompson theorem:

https://plus.google.com/u/0/117663015413546257905/posts/4BZRibN6iKQJun 30, 2013 - I have been following this book for a year, it has been a truly amazing year indeed! I highly recommend everyone here buys a copy! oh btw, its Coq and Agda 2 now ;) don't forget Idris with dependent types +John BaezJul 12, 2013
- Jul 12, 2013