It's also important to note that this situation is _precisely_ what Voevodsky wanted to prevent: For nearly a decade, Voevodsky has been advocating the virtues

It's also important to note that this situation is _precisely_ what Voevodsky wanted to prevent: For nearly a decade, Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of mathematics and computer programming closer together. As he sees it, the move to computer formalization is necessary because some branches of mathematics have become too abstract to be reliably checked by people. “The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes,” Voevodsky said. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error. [1] Most mathematicians still think of machine check for dealing with a large _number_ of cases; but Homotopy Type Theories goal is to manage abstract complexity not just size. [1]https://www.quantamagazine.org/univalent-foundations-redefines-mathematics-20150519/ https://www.quantamagazine.org/univalent-foundations-redefin...