A consortium of today's greatest mathematicians have laid out new foundations. They all lie upon one single axiom, called univalence. With univalence, our Arabic numbers aren't just like natural numbers; They are natural numbers. Univalence also has unforeseen and mesmerizing consequences.
In this article, we explore the possibilities allowed by higher inductive types. They enable a much more intuitive formalization of integers and new mind-blowing definitions of the (homotopical) circle and sphere.
In 2013, three dozens of today's brightest minds have laid out new foundations of mathematics, which better fits both informal and computationally-checkable mathematics. Have a primer of this upcoming revolution, with this article on type theory, the theory that the book builds upon!
Take a square sheet of paper. Can you glue opposite sides without ever folding the paper? This is a conundrum that many couldn't figure out. While John Nash did answer yes, he couldn't say how. Finally in 2012, Borrelli and his collaborators finally made it! And it is spectacularly beautiful!