Unlike computer code, there is no huge repository of formalized proofs to train a machine learning algorithm on. Furthermore for interactive proof assistants (C

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.