What are possible applications of deep learning to research mathematics? With no doubt everyone here has heard of deep learning, even if they don't know what it is or what it is good for.  I myself am a former mathematician turned data scientist who is quite interested in deep learning and its applications to mathematics and symbolic reasoning.  There has been a lot of progress recently, and while it is exciting to machine learning experts, the results so far are probably not useful for research mathematicians.  My question is simple:
Are there areas of research math, that if one had access to a fully trained state-of-the-art machine learning model (like the ones I will describe below), it would make a positive impact in that field?
While math is mostly about proofs, there is also a need sometimes for computation, intuition, and exploration.  These are the things that deep learning is particularly good at.  Let me provide some examples:
Good intuition or guessing
Charton and Lample showed that Transformers, a now very standard type of neural network, are good as solving symbolic problems of the form
$$ \mathit{expr}_1 \mapsto \mathit{expr}_2 $$
where $\mathit{expr}_1$ and $\mathit{expr}_2$ are both symbolic expressions, for example in their paper $\mathit{expr}_1$ was an expression to integrate and $\mathit{expr}_2$ was its integral.  The model wasn't perfect.  It got the right answer about 93-98% of the time and did best on the types of problems it was trained on.  Also, integration is a 200 year old problem, so it is hard to outcompete a state-of-the-art CAS.
However, there are some things which make this interesting.  Symbolic integration is important, difficult, and (somewhat) easy to check that the solution is correct by calculating the derivative (and checking symbolically that the derivative is equivalent to the starting integrand).  Also it is an area where “intuition” and “experience” can definitely help, since a trained human integral solver can quickly guess at the right solution.  Last it is (relatively) easy to compute an unlimited supply of training examples through differentiation.  (This paper also uses other tricks as well to diversify the training set.)
Are there similar problems in cutting edge mathematics, possibly in algebra or combinatorics or logic where one would like to reverse a symbolic operation that is easy to compute in one direction but not the other?
Neural guided search
Some problems are just some sort of tree or graph search, such as solving a Rubik's cube.  A neural network can, given a scrambled cube, suggest the next action toward solving it.  A good neural network would be able to provide a heuristic for a tree or graph search and would prevent exponential blow-up compared to a naive brute-force search.  Indeed, a paper in Nature demonstrated training a neural network to solve the Rubik's cube from scratch this way with no mathematical knowledge.  Their neural network-guided tree search, once trained, can perfectly solve a scrambled cube.  This is also similar to the idea behind AlphaGo and its variants, as well as the idea behind neural formal theorem proving—which is really exciting, but also not up to proving anything useful for research math.
Puzzle cubes and board games are not cutting edge math, but one could imagine more interesting domains where just like a Rubik's cube one has to manipulate one expression into another form through a series of simple actions, and the ability to do that reliably would be of great interest.  (Note, the neural guided tree search I've described is still a search algorithm and much slower than a typical cube solving algorithm, but the emerging field of program synthesis could possibly one day soon learn from scratch a computer program which solves the Rubik's cube, as well as learn computer programs to solve more interesting math problems.)
Neural information retrieval
Suppose you have a database of mathematical objects (say, integer sequences, finite groups, elliptic curves, or homotopy groups as examples) and you want a user to be able to look up an object in this database.  If that object is in the database, you would like the user to find it.  If it is not, you would like the user to find similar objects.  The catch is that "similar" is hard to define.  Deep learning provides a good solution.  Each object can be associated with an embedding, which is just a vector in, say, $\mathbb{R}^{128}$.  The measure of similarity of two objects is just the inner product of their embeddings.  Moreover, there are a number of techniques using self-supervised machine learning to construct these embeddings so that semantically similar objects have similar embeddings.  This has already shown a lot of promise in formal theorem proving as premise selection where one wants to pick the most relevant theorems from a library of theorems to use in the proof of another theorem.
For example, I think such a neural database search could reasonable work for the OEIS, where one can use a neural network to perform various prediction tasks on an integer sequence.  The inner layers of the trained network will compute a vector embedding for each sequence which can be used to search through the database for related sequences.
Geometric intuition
Neural networks are pretty good at image recognition and other image tasks (like segmentating an image into parts).  Are there geometry tasks that it would be useful for a deep learning agent to perform, possibly in dimensions 4 or 5, where human geometric intuition starts to fail us since we can't see in those dimensions.  (It would be hard to make, say a convolutional neural network work for a 4 dimensional image directly, but I could imagine representing a 3D surface embedded in 4D as say a point cloud of coordinates.  This could possibly work well with Transformer neural networks.)
Build your own task
Neural networks are very flexible when it comes to the choice of input and output, as well as the architecture, so don’t let the specific examples above constrain your thinking too much.  All you need are the following things:

*

*A type of mathematical object.  One that you care about. It should be representable in some finite way (as a formula, an initial segment of a sequence, an image, a graph, a computer program, a movie, a list of properties).

*A task to perform on your operation.  It can be well specified or fuzzy.  It can be solvable, or (like integration) only partially solvable.  It can be classifying your objects into finitely many buckets.  It could be computing some other related object or property of the object.  It could be finding the next element in a sequence.  It could be coming up with a prediction or conjecture of some sort.  It could be turning that object into a some 2D cartoon image even, just to think outside the box.

*Lots of training data.  Either you need to be able to synthetically generate a lot of training examples as in the integration example above, or like OEIS have a large dataset of 10s of thousands or examples (more examples is always better). Clean data is preferred but neural networks handle messy data very well.  Another “data free” solution is reinforcement learning like in the Rubik’s Cube example or AlphaGoZero, where the agent learns to explore the problem on its own (and generates data through that exploration).

*Patterns in the data, even if you can’t see what they are.  Your task should be one where there are patterns which help the machine learning agent solve the problem.  (For example, I’m not convinced that factoring large integers would be a good task.)

*Motivation.  Why would this be useful to the field?  What purpose would having this trained model have?  Would it make it easier to conjecture facts, explore new areas of math, wrap ones head around a bunch of confusing formulas?  Or do you have a way to turn a learned heuristic into a proof, such as with a search algorithm (as in the Rubik’s cube example above) or by checking the solution (as in the integration example above)?

 A: There has been some recent efforts in utilizing neural networks to approximate solutions of different types of PDEs. The key advantage of this approach is the possibility of tackling extremely high-dimensional problems, where traditional numerical approach involving discretization proves infeasible as the number of grid points scales exponentially with dimension.
Deep learning approaches sidestep the curse of dimensionality by converting the PDE problem into e.g. minimizing an energy functional https://arxiv.org/abs/1710.00211 or a stochastic optimal control problem https://arxiv.org/abs/2102.11379, then solve the related ERM problem via Monte Carlo sampling, whose convergence is independent of dimension.
A: One application that we urgently need is a "smart" catered TeX-math search engine (eg.an interesting one is https://approach0.xyz/search/ ).

*

*achieving a collaboration with the people in arxiv to have the engine search through the TeX code of math papers. (So maybe even coming up with some template of math-TeX glossary that we should follow if we want to ease searchability).

*So this would require an engine that is flexible and even present us with search-results that are close but from different areas, establishing interesting bridges.

*I imagine the AI would also be useful here in forming a loose family of theorems and definitions based on topic. Thus giving us a sense of the various directions in math.

Another interesting application would be to help in PDEs with sharpening the various constants. I imagine a really smart AI would be great for running through a wide range of candidate functions and having the cost function just be based on the sharpening of the constant.
A: Full disclosure: This is a copy-and-paste of my answer to a question over on CrossValidated (stats Stack Exchange).
See the 2019 preprint Machine Learning meets Number Theory:
The Data Science of Birch-Swinnerton-Dyer by Alessandretti, Baronchelli & He. Here is the Abstract:

Empirical analysis is often the first step towards the birth of a conjecture.
This is the case of the Birch-Swinnerton-Dyer (BSD) Conjecture describing
the rational points on an elliptic curve, one of the most celebrated unsolved
problems in mathematics. Here we extend the original empirical approach, to
the analysis of the Cremona database of quantities relevant to BSD, inspecting
more than 2.5 million elliptic curves by means of the latest techniques in data
science, machine-learning and topological data analysis.


Key quantities such as rank, Weierstrass coefficients, period, conductor,
Tamagawa number, regulator and order of the Tate-Shafarevich group give rise
to a high-dimensional point-cloud whose statistical properties we investigate.
We reveal patterns and distributions in the rank versus Weierstrass coefficients,
as well as the Beta distribution of the BSD ratio of the quantities. Via gradient
boosted trees, machine learning is applied in finding inter-correlation amongst
the various quantities. We anticipate that our approach will spark further research on the statistical properties of large datasets in Number Theory and
more in general in pure Mathematics.

A: In the context of algebraic geometry, neural networks have become useful tools in the study of Calabi-Yau manifolds. The computation of their topological invariants, metrics and volumes is of particular interest for applications in physics (string theory). Recent contributions include

*

*Machine learning
Calabi-Yau metrics

*Machine learning Calabi-Yau
four-folds

*Deep learning Calabi-Yau metrics

*The Calabi-Yau Landscape: from Geometry, to Physics, to Machine-Learning

For a more general overview, see Machine-Learning Mathematical Structures

We review, for a general audience, a variety of recent experiments on
extracting structure from machine-learning mathematical data that have
been compiled over the years. Focusing on supervised machine-learning
on labeled data from different fields ranging from geometry to
representation theory, from combinatorics to number theory, we present
a comparative study of the accuracies on different problems. The
paradigm should be useful for conjecture formulation, finding more
efficient methods of computation, as well as probing into certain
hierarchy of structures in mathematics.

A: 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.
A: In the category of guessing, there is the Ramanujan Machine. This project got off on the wrong foot with the research mathematics community because their initial announcement made overblown claims (such as claiming novelty for some conjectures/theorems that weren't new), but it is my belief that the general concept is sound.  Along similar lines, perhaps it's time to revisit Graffiti with modern neural nets.  In his paper On Conjectures of Graffiti (Ann. Discrete Math. 38 (1988), 113–118), Siemion Fajtlowicz described a computer program for generating conjectures about finite graphs.  Most of its conjectures were either false, trivial, or known, but it did come up with some novel conjectures that were interesting enough for graph theorists to spend time proving them and publishing the proofs.
In the category of guided search, people have tried to use neural networks to improve the performance of SAT solvers; see for example the work on NeuroSAT.  This seems like a promising area for further research.
A: Neural networks might help to speed up computations in the monster group
$\mathbb{M}$, which is the largest finite sporadic simple group. Such a
network could be in some sense a (rather large) cousin of the neural network
dealing with Rubik's cube mentioned by the OP.
Elements of $\mathbb{M}$ are usually represented as words of sparse matrices
in  $\mbox{GL}_n(\mathbb{F}_k)$, $196882 \leq n \leq 196884, k = 2,3$.
There is
an effective algorithm for checking equality of two such words, see [1]. Reduction of a word to a shorter word may take several minutes on a computer,
see e.g. [2] for an overview. I'm currently working on the acceleration of
the reduction of such words. I plan to exploit some geometric information
contained in the images of certain vectors in $\mathbb{F}_k^n$. As far as
I know, nobody has used this information before.
(For experts: I focus on the images of vectors called 2A-axes).
Here a neural network might be better at learning how to use this
information than I am.
The mathematical benefits of such a project are:

*

*Regarding computations, the monster group is the most difficult finite
simple group to deal with.
If we can compute in the monster group then we can compute in all finite
groups, provided we have enough information about that group and enough computer memory.


*We can probably finish the classification of the maximal subgroups of
the monster group.
References
[1] R. Wilson. Computing in the monster. In Group, Combinatorics & Geometry, Durham 2001, 327–337. World Scientific Publishing, 2003.
[2] R. A. Wilson.
The Monster and black-box groups.
A: Some recent work on neural formal theorem proving (already mentioned in the question, but the examples give a sense of the state of the art):

*

*Generating correctness proofs with neural networks

*Mathematical Reasoning via Self-supervised Skip-tree Training

*TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
A: This predates deep learning, but we should not forget that there has already been
some progress in graph theory by recognizing patterns
(OP: "patterns in the data")
and forming conjectures.

*

*Hansen, Pierre, and Gilles Caporossi. "AutoGraphiX: An automated system for finding conjectures in graph theory." Electronic Notes in Discrete Mathematics 5 (2000): 158-161.
DOI.


"Up to now it [AutoGraphiX] has refuted 9 conjectures of Graffiti and suggested over 50 novel conjectures, 15 of which have been proved and none disproved."

Just posted (29Apr2021):
A.Z. Wagner, "Constructions in combinatorics via neural networks."
arXiv abs:

"We demonstrate how by using a reinforcement learning algorithm, the deep cross-entropy method, one can find explicit constructions and counterexamples to several open conjectures in extremal combinatorics and graph theory."

As requested, now a separate post.
A: Adam Wagner has a new paper on arXiv (29 Apr 2021), "Constructions in combinatorics via neural networks," whose
Abstract is:

"We demonstrate how by using a reinforcement learning algorithm, the deep cross-entropy method, one can find explicit constructions and counterexamples to several open conjectures in extremal combinatorics and graph theory.
Amongst the conjectures we refute are a question of Brualdi and Cao about maximizing permanents of pattern avoiding matrices, and several problems related to the adjacency and distance eigenvalues of graphs."

Will Sawin commented here that "Wagner's paper refutes a conjecture by AutoGraphiX" (and deserved to be in an answer of its own).
Timothy Gowers discussed this on Twitter, summarizing that "the rough idea of the program is to design a suitable reward function, usually very simple, for how good an attempted counterexample is, and let the magic of reinforcement learning do the rest".
A: Neural networks are also just starting to be used in knot theory!
One of the largest unsolved parts of the field is finding the structure of the smooth Knot Concordance Group. Doing so requires a firm understanding of many knot invariants, chief of which are the $\tau$ and $s$ invariants of Ozsváth, Szabó, and Rasmussen. These are powerful invariants, both of which are derived from the intrinsic geometry of the knot in question, yet they are very difficult to compute for complicated knots.
The problem of computing these invariants is very conducive to the use of neural networks: there is a large training set (all knots where the computation has already been carried out) and a root in the geometry of the object. Lastly, I would be remiss not to mention that the calculation of these invariants is part of a large scale computational strategy for finding a counterexample to the Smooth 4-dimensional Poincaré conjecture. This is commonly regarded as the largest remaining question in low dimensional topology.
