A.I. Is Coming for Mathematics, Too

Unlike computer code, there is no huge repository of formalized proofs to train a machine learning algorithm on. Furthermore for interactive proof assistants (Coq, Lean, and others), the code saved on disk does not contain any of the intermediate goals, which is necessary for understanding the proof structure.

If machine learning makes inroads into pure mathematics, it will have to be from some sort of reinforcement learning, not supervised learning.

I've been thinking about this since AlphaDev, but the same sort of program that can build sorting algorithms can also prove math theorems using an automated proof checker. The real question is if it can be used to prove something significant, not just trivial findings.

For me, this is one of the core tests for true AI. Can a machine discover and communicate logical structures/relationships that humans have never seen before? That is when I will actually be scared.

Yeah. Right.