(See the sibling comment with a "10." in it for context.)

6. The Growth of Univalent Foundations/ Homotopy Type Theory. This is the bastard offspring of (semi-)automatic proof checking, the "foundations of mathematics", and, of all things, topology. The connection between these may become less surprising if you are familiar with category theory, which has always been kinda foundational and kinda topological.

I don't really know anything about this stuff, and unlike (e.g.) inter-universal Teichmueller theory or the Langlands program I can't really claim that that's because it's beyond human comprehension :-). I bet there are people here who know a lot more than I do about this, and I hope they'll correct my mistakes and fill in my gaps. Anyway, it goes something like this:

Mathematicians have always liked building complicated things out of simple things, and in particular have always wanted to build the whole of pure mathematics on top of something nice and simple. The traditional nice-and-simple thing to use for this has been set theory; the study of collections of things. The usual path from raw sets to the mathematical objects we're familiar with -- which is not relevant to "univalent foundations", so skip this if you like -- goes like this. First, build a structure to serve as your non-negative integers. Zero will be the empty set; n+1 will be {0,...,n}. Define addition and multiplication "by induction". Next, ordered pairs: if a,b are sets then {{a},{a,b}} is a set from which you can work out what a,b were. Abbreviate that as (a,b). Now we can make the integers as follows: consider ordered pairs (a,b) where a,b are nonnegative integers, and interpret them as meaning a-b. We need to treat (a1,b1) and (a2,b2) as the same when a1-b1=a2-b2, which is the same as a1+b2=a2+b1, which is a statement only about nonnegative integers and addition. Now we can make rational numbers: take ordered pairs (a,b) where a,b are integers and b isn't zero, meaning a/b; again (a1,b1) and (a2,b2) are the same when a1/b1=a2/b2, which is the same as a1.b2=a2.b1, which is a statement only about integers and multiplication. Now make real numbers by "Dedekind cuts"; the real number x "is" the set of all rational numbers < x. Etc., etc., etc.

There are some not-so-likeable things about basing mathematics on set theory. One is that the notion of "set", although it seems absolutely straightforward and transparent, turns out to be not so much so when you look more closely. E.g., you might think that for any proposition P with a single "free variable" x in it, there should be a set of "all x such that P". E.g., "all x such that x is a prime number". But that famously can't work in general; take P = "x is a set that doesn't have itself as a member" and you get a paradox. So you have to restrict your ability to form sets in this way, and there are a bunch of different ways of doing it, and none of them is perfectly satisfactory.

(A certain amount of unsatisfactoriness is inevitable thanks to Goedel's incompleteness theorem. However you try to construct mathematics, either your system will just be broken or else there will be questions it can't resolve.)

"Univalent foundations" is an entirely different approach. The idea is to build mathematics on something like the lambda calculus -- that is, roughly, you start with functions rather than objects. You can very very handwavily say that the relationship between u.f. and traditional set-theoretic foundations is a teeny little bit like that between Haskell and, say, C.

One of the cute things about lambda calculus is a theorem that connects types with mathematical theorems, and expressions that compute a value of a given type with proofs of the corresponding theorems. This is at the heart of proof-checking systems like Coq and Agda. And one of the ideas behind univalent type theory is to find a type system rich enough that you can use this for talking about all of mathematics.

I've not really got very far into talking about UTT but I'll stop here because (see above) I don't really know what I'm talking about and I'm sure other people on HN know it much better. The hope is to provide foundations for mathematics that (1) don't have so many layers of arbitrary construction between the foundations and the things mathematicians actually use, and (2) are amenable to automated checking. I think.