Type theory and formalization of mathematics