What We Know
According to a World Bank page, "Today, there are around 200 million higher education students in the world, up from 89 million in 1998." At least 1 in 100 have, as a mathematics requirement, had to develop a proof for a theorem, and live at least 40 years afterward.
Although there are at least 20 million neural nets that can prove a theorem, they fall short of examples that would answer this question in the affirmative. These neural networks are biological, not artificial, and they have mostly proven previously proven theorems, not the Collatz conjecture or the Riemann conjecture.
What Some Believe
Those who believe that deep Q-learning and attention based devices will be joined by other learning system designs until the faculties of the human brain are simulated and perhaps surpassed, would likely include theorem proving as one of those human capabilities. These would likely declare predicate logic and inference as just another complex cognitive function that will be achieved in artificial systems.
Those who believe that some capabilities are imbued into humans and are reserved capabilities, may declare predicate logic and inference as reserved to humans alone.
Current State of Progress
There are no academic articles indicating the ability to prove even the simplest proofs using predicate logic and inference. It is possible that a government or private enterprise has achieved some level of success in doing so, but such has not been disclosed.
The idea that artificial networks, if developed appreciably, could surpass production systems, AI systems that are abased on productions or rules, in their areas of greatest effectiveness was proposed early in the development of AI. It was disputed then and disputed now, however the arguments are not mathematical, so there is no strong indication that it is impossible.
Certainly other cognitive aspects of human thought are important objectives of AI research. Dialog, automated education, planning, strategic analysis, and vehicle piloting are all aspects of higher thought that demand more than DQN and attention based network approaches can now deliver, but the research effort in these areas are appreciable and well funded.
Research toward logical cognitive abilities should begin proofs already know, far simpler than the conjectures mentioned in the question. For example, it has been proven that the sum of two non-negative integers must be another non-negative integer. In predicate calculus, that can be represented as a character string.
∀ a∈C, b∈C: s=a+b ⇒ s∈C
It says that a and b being members of the set of counting numbers, that the s, defined as the sum of the two, must also be a member of the set of counting numbers. It's proof can also be represented as a sequence of character strings of first order predicate calculus.
No Small Research Project
Such an example may seem simple to someone who has taken years of math courses and has constructed proofs. It is not simple for a child, and it is very difficult to get an artificial network to converge to a function that applies all the rules of logical inference and incorporates meta-rules for arriving at a proof for a formal system such as integer arithmetic.
Turing complete networks, such as RNNs, will certainly have advantages over MLPs (multilayer perceptrons). Attention based networks may be a reasonable research option. There are others indicated in the references below.
A parallel computing platform would be needed for the research, since the input vector may be hundreds of Kbytes. The sizes of examples and how many would be needed is difficult to estimate without getting a year or two into the research process.
The definition of counting numbers, the plus sign, and the equals sign must first be defined, and those definitions and a number of axioms, postulates, lemmas, and corollaries must be part of the input example in the formal form like the proposal to be proved above, along with that proposal.
And that's the work to prepare only one example. You'd need thousands to train intuitive knowledge about the rules of inference into a deep network. (I chose the word INTUITIVE very deliberately for theoretical reasons that would take at least a hundred pages to explain well.)
This is no small project since the example data set must have at least a few thousand cases, and each case, though it may share some theory, must be set up so that the proposal is perfectly formed and the necessary body of theory is also presented in perfect form at the input for each training iteration.
My guess is that it would take a team of bright researchers with the appropriate understanding of deep networks, convergence, and predicate calculus about ten years to train a network to give viable proofs in response to simple mathematical proposals.
But It Would Be No Small Achievement
That may seem an absurd endeavor for some, but it would be the first time someone taught a computer how to be logical. It took nature just under the age of earth to teach logical inference to an organism, Socrates.
People assume that because a computer is made up of digital circuits that perform logic by design that computers are logical. Anyone who has been around software development for decades with the inclination to think deeper than hacking for fun or money knows differently. Even after careful programming, computers do not simulate logical inference and cannot correct their own programmed behavior for any arbitrary bug. In fact, most of software development today is bug fixing.
Simulating logical thought would be a major step toward simulating cognition and the wider array of human capabilities.
Learning to Compose Neural Networks for Question Answering
Jacob Andreas, Marcus Rohrbach, Trevor Darrell, and Dan Klein
Learning multiple layers of representation
Geoffrey E. Hinton
Department of Computer Science, University of Toronto
Neural Turing Machine (slideshow)
Author: Alex Graves, Greg Wayne, Ivo Danihelka
Presented By: Tinghui Wang (Steve)
Neural Turing Machines (paper)
Alex Graves, Greg Wayne, Ivo Danihelka
Reinforcement Learning, Neural Turing Machines
Wojciech Zaremba, Ilya Sutskever
ICLR conference paper
Dynamic Neural Turing Machine with
Continuous and Discrete Addressing Schemes
Caglar Gulcehre1, Sarath Chandar1, Kyunghyun Cho2, Yoshua Bengio1
An On-Line Self-Constructing Neural Fuzzy, Inference Network and Its Applications
Chia-Feng Juang and Chin-Teng Lin
IEEE Transactions on Fuzzy Systems, v6, n1
Gated Graph Sequence Neural Networks
Yujia Li and Richard Zemel
ICLR conference paper
Building Machines That Learn and Think Like People
Brenden M. Lake, Tomer D. Ullman, Joshua B. Tenenbaum, and Samuel J. Gershman
Behavioral and Brain Sciences
Context-Dependent Pre-Trained Deep Neural Networks for Large-Vocabulary Speech Recognition
George E. Dahl, Dong Yu, Li Deng, and Alex Acero
IEEE Transactions on Audio, Speach, and Language Processing
Embedding Entities and Relations for Learning and Inference in Knowledge Bases
Bishan Yang1, Wen-tau Yih2, Xiaodong He2, Jianfeng Gao2, and Li Deng2
ICLR conference paper
A Fast Learning Algorithm for Deep Belief Nets
Geoffrey E. Hinton, Simon Osindero, Yee-Whye Teh (communicated by Yann Le Cun)
Neural Computation 18
FINN: A Framework for Fast, Scalable Binarized Neural Network Inference
Yaman Umuroglu, et al
From Machine Learning to Machine Reasoning
Yann LeCun1,2, Yoshua Bengio3 & Geoffrey Hinton4,5
Nature vol 521