Yep, there is a lot of cool stuff on formalizing maths rigorously, called informally 'computer mathematics'. We give a brief overview of this work in our papers

Yep, there is a lot of cool stuff on formalizing maths rigorously, called informally 'computer mathematics'. We give a brief overview of this work in our papers. Moreover, for the interested reader, I would suggest paying close attention to univalent foundations of mathematics (http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html 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.