But I agree that many problems are not suited for machine learning since they are too easy or too hard. Nonetheless, math is a diverse subject and I think there is a lot of areas of math where machine learning would be a good fit, especially if one realizes how powerful and flexible it has now become. The challenge is pairing up the folks who know about the problems with the folks who know the machine learning solutions that might help.

As for your first point, I think it is too simplistic to assume that supervised learning problems of interest have to be the type of problems for which a formula can even exist. For example it doesn't make sense to talk about a "formula" for computing a symbolic integral. Also, maybe one wants to compute a value from a representation matrix (like in the CY manifold example above). Again, a formula doesn't seem like the right type of solution. Maybe there is an algorithm, but it is quite possible that this algorithm is hard to find, and having an approximate solution would be a good start.

@CarloBeenakker Are you interested in making an answer just for that survey paper since it goes beyond CY manifolds? Or if you like I can do it.

@CarloBeenakker This is really general. From that paper: "We emphasize again that the computing a topological invariant of any manifold (appropriately embedded as an algebraic variety) can be cast into the form of [a simple machine learning training problem]. We turned to CY because of their being readily available [data], similar experiments should be carried out for general problems in geometry." (Although I don't know enough about this area to say if it is surprising or useful.)

@მამუკაჯიბლაძე, have a look at arxiv.org/pdf/1805.11799.pdf which trains a neural theorem prover for intuitionistic propositional logic. (Although, you may also want to check out some intuitionistic ATPs, like some of the powerful tactics in Coq that may be better suited for your use case.)

@მამუკაჯიბლაძე, yes there are a number of papers on machine learned theorem provers (see one of the answers below). Do you think that they would help you in your or others research? You mentioned wanting a theorem prover for intuitionistic propositional logic. That is an interesting use case, since for classical propositional logic, I suspect SAT solvers still reign supreme, but for less common logics it may be easier to build a solver directly from training data.

@WillSawin, I haven't been clear. I greatly value Buzzard's work and his predecessors. I played a small role in Hale's formalization of the Kepler Conjecture, and a much larger role in lean-gptf, a recent neural theorem proving tactic for Lean (Kevin's prover of choice). What I want to emphasize here is that we don't have to solve automatic theorem proving (a REALLY hard problem) to use AI to solve outstanding math problems right now. I also don't think lean-gptf and such will currently solve new theorems or create new insights, but neural tools focused on specific areas of math will.

This is a great example! I was expecting only to get ideas for future research (and that is still what I’m looking for) and not already published results, so this is very motivating. Could you possibly elaborate on the task being performed here? I don’t know much about this area, but it seems that in the second example the input to the NN is a matrix of integers representing a class of manifolds and the output is an integer hodge number from 1 to 24 of that class. Is that correct? What about the first example?

While I think such work provides a lot of motivation and encouragement, I don't think it is currently useful to research math and I don't think it will be for a while. However, I think there are probably more specific applications of machine learning to specific areas of mathematics that could be of value right now if we find them.

And all of Josef Urban's work.

Also see TacticToe (HOL4), Tactitian (Coq), CoqGym/ASTactic (Coq), HOList/DeepHOL (HOL Light), Holoprasm (Metamath), GPT-f (Metamath), Lean GPT-f (Lean) for more state of the art in this area.

I'm one of the authors of the lean-gptf paper. :) I'm very encouraged by the progress in machine learning on formal mathematics libraries, but I think it has a long way to go to help work-a-day mathematicians. On the other hand, I think there are probably more focused applications of deep learning to specific areas of mathematics that could have an impact right now, or relatively soon.

@TimothyChow When you say " tell whether a particular theorem can be proved in Zermelo set theory (ZF minus Replacement)", I assume you don't mean that exactly, because that isn't even easily possible with the logic ZFC. I think you mean something like "tell whether the axioms used in the proof are logically no stronger than ZF-Replacement", right? However, even if this is possible, it likely isn't going to be of a lot of value, since practical ITP projects (esp. in Lean) often use more axioms than strictly necessary, e.g. AC, for convenience.