"the development of mathematics within a type-theoretic foundation (including both previously existing mathematics and new mathematics that homotopical types make possible)"

I'm sure Mr Hilbert would approve.

"and the formalization of each of these in computer proof assistants."

Aah, loosely IT related (hence the post) and surely Lean and co can't be far away from the discussion.

"As such, this article may not represent the views of all researchers in the fields equally. This kind of variability is unavoidable when a field is in rapid flux."

The WP article is quite dense for a civilian to get through so I hope something cool is on the horizon.

Is a result on the way or has Lean blue screened?