I have some thoughts on a level of generality that is a bit higher than the question asks for:
One obstacle that faces applications of supervised machine learning to predict properties of mathematical objects is that in many fields of mathematics, such as number theory, we tend to expect that properties of the nice mathematical objects we study will either be
- given by explicit formulas, or
- quasirandom and hard to predict.
If this expectation is correct, then machine learning researchers are in a bit of a bind - they will either discover nothing or something trivial. Of course, mathematicians are fallible and our expectations are certainly not always correct.
This suggests one approach would be to use neural networks to search for properties that are unexpectedly easy to predict. This would be a somewhat thankless task as you would usually find nothing of interest, but when you do find something it would be a counterintuitive new phenomenon, which could hopefully by human analysis turned into a new formula for something.
It is crucial in this setting to have a good understanding of existing quasirandom models of the object in question, to know what trivial bounds your prediction is trying to beat. (This has been a pitfall for some attempts to apply machine learning, or just classical statistics, to pure mathematics.)
I am particularly excited about bringing techniques from puzzles and games to pure math, as in the neural guided search section of the question. This is because neural networks on games are some of the only networks to not just achieve human performance on tasks, and not just achieve superhuman performance, but to achieve superhuman performance by introducing new ideas which human practitioners were able to learn from and incorporate into their own strategies.
Since the goal of mathematics is the production of ideas, this is very heartening.
So we're looking for games where one must apply a sequence of moves, following some rules, to try to reach some result. (I don't know many examples of adversarial games in pure mathematics, so I'm describing 1-player games.)
Formal theorem proving is an example of this, already discussed in Steve Huntsman's answer.
I believe Kirby calculus is a game or puzzle of this sort, with the goal of showing two 3-manifolds or 4-manifolds are diffeomorphic by a finite series of combinatorial moves, that is used in current research (to test whether a newly constructed smooth structure on a 4-manifold is exotic or diffeomorphic to the standard structure). One challenge might be finding a good way to represent the diagrams that a network can work with efficiently.