This is really cool, but I was hoping that they were going to formalize mathematics. For example, like this ([1]) team is doing.
Mathematics should primarily read like code, not (only) like prose.
Mathematics should primarily read like code, not (only) like prose.
Moreover, for the interested reader, I would suggest paying close attention to univalent foundations of mathematics (http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundation...) introduced by Vladimir Voevodsky. It disrupts classical derivation of math results rooted in Kantor's set theory and logics, and provides a theoretical framework that is much more convenient for computerizing.
Unlike them, we follow the different, less theoretical and more pragmatic, approach.