Will Computers Redefine the Roots of Math?
&gt; “The drive to mechanize proof and proof verification doesn’t strongly motivate most mathematicians as far as I can tell,” he [Michael Harris] said. “I can understand why computer scientists and logicians would be excited, but I think mathematicians are looking for something else.”<p>I&#x27;m not a mathematician, but I have at times been able to consider myself a computer scientist. To me, the goal of &quot;mechanizing&quot; and formalizing mathematics seems instinctively recognizable as a worthwhile pursuit, for the same reason it&#x27;s worth adding tests to an unwieldy legacy codebase: it makes it possible to refactor, to experiment and break things and see what happens.<p>The more we formalize the most fundamental axioms and theorems of mathematics, the more confidently we can alter or remove them and see what happens to the rest of the system. Achieving &quot;100% test coverage&quot; and &quot;instrumentation&quot; of mathematics would allow us to analyze the system under stress. We could fuzz it. We could refactor it. We could even ask an AI to do that for us.<p>As a relative layman, I&#x27;m often struck by how many mathematical theorems are dependent on the arbitrary paths we took to develop them. For the same reason, it&#x27;s a common occurrence that one mathematician discovers an innovation in one branch of mathematics by simply borrowing a common technique from a distantly related branch. Those sorts of analogies and connections between ideas are difficult for humans to spot, and their discovery scales linearly with the number of mathematicians, who might prefer to spend their time discovering truly new ideas rather than repurposing those already existing ideas.<p>But computers, on the other hand, are excellent at spotting these relationships, if given sufficiently formalized definitions of them. So that&#x27;s why I&#x27;d be most excited about formalizing mathematics:  how much low-hanging fruit is waiting to be discovered by computers that are just missing the right prompt?