Madhusudhan Raman

Peter Sarnak’s writes in the Notices of the American Mathematical Society on the “AlphaZero Test” for AI in mathematics:

The AlphaZero Test: The theorem prover has no access to any outside data or theory, and we input the statement of [some explicit and elementary conjecture] and we ask the theorem prover to decide if it is true or false. I postulate that it will fail the test… That is, the process of generating proofs toward a goal via self-correcting guesses using statistical machine learning… will recover few of the theorems of our theories.

Rather disappointingly, Sarnak goes on to write:

If the postulate is wrong, the impact on mathematics would be dramatic since we would be in the position of knowing that statements of great interest to us are true (proven!) but not understanding why. Since understanding is such an integral part of doing mathematics, we will have to rethink what mathematics is.

This may be naïve, but it seems to me that having an oracle that certifies (reliably, even) the truth or falsity of mathematical statements doesn’t change what a mathematician would do to understand why it is true or false. The mathematician would go from saying “I am trying to prove this conjecture/find a counterexample to this conjecture” to “This conjecture is true/false and I am trying to understand why.” In both cases, the mathematics is the understanding.

Sarnak goes on to postulate that:

The problems for which [our statistical theorem prover] will have success are ones that are already in the ballpark of our current theories — “the elementary statistical derivatives of the theories.” Indeed, these are the problems that most of us try to solve, most of the time. The proving device will expedite the determination and understanding of what these are and serve as an assistant in resolving them.

This is something David Bessis has argued more persuasively elsewhere. Perhaps the analogy with chess engines is useful, though.