The mathematics being discussed here is very new, as well as very technical, and I would guess the number of people who really understand it at the moment is at

The mathematics being discussed here is very new, as well as very technical, and I would guess the number of people who really understand it at the moment is at most dozens; certainly fewer than hundreds. I am certainly not one of those people. Nevertheless, I find this enormously exciting. Formalisation of mathematics has long been the preserve of a handful of logicians and type theorists. What we’re seeing here is one of the world’s leading mathematicians, whose work is situated squarely at the centre of what is today considered mainstream mathematics, advocating the importance of formalisation. If, like me, you believe that formalisation will be an essential part of the mathematics of the future, this is a very encouraging development.