# Application of Machine Learning to the Automated Theorem Proving

I am very interested in developing a machine-learning algorithm that could learn from the axioms, properties, and examples of the mathematical conjectures of interest to generate possible key properties of possible proofs, which AI could then deduce the proof sketches. I am curious what kind of research has been done on those topics as I have an impression that there has not been many research since recent years.

If I would like to come up with a proof for Jacobian Conjecture, does learning algorithm have to learn everything about the prerequisite materials, such as commutative algebra, set theory, and analysis? How does it work?

• I'd like to link Q: machine learning applications in number theory. It asks something similar specifically for Number Theory. – Jim May 15 '18 at 16:47
• ML algorithms are good at finding patterns in the data, the question you should ask yourself is if you can find proofs for theorems by pattern recognition. Many would argue, that this needs an in-depth understanding of the problem, so you'd probably need a strong AI in here, and as for now, we don't have anything even close to it. – Tim May 15 '18 at 19:52
• I'm gonna code me up of those Machine Learning Automated Theorem Proving thingies. I'll shake it out on the Riemann Hypothesis. Then tomorrow, I'll prove P = NP (or not). – Mark L. Stone May 15 '18 at 20:23
• – kenorb Nov 30 '18 at 13:33

Recent papers I know of are Deep Network Guided Proof Search and Deep Math. Both of these reduce the search-space of current non-ML based theorem-provers by suggesting the next premise or tactic to use, pruning the search tree. (Quite similar to how Alpha Zero still relies on traditional game-tree search, but heavily prunes it!)

A more direct approach taken by End to End Differentiable Proving focuses on the backward chaining proof search technique. It replaces the hard decision of which variable to substitute into which rule (for example: substitute "John" into the rule: If Human(x) then Alive(x)) with a scoring function which assigns a number to how good each possible substitution is. Then a beam-search is used to find the highest scoring set of substitutions.

I would contest the idea that finding proofs can't be solved using pattern recognition -- I rely on a lot on my intuition when proving things, which pretty much just guesses which direction to try next based on similar problems I've seen before. This approach seems quite similar to above papers. In other words, my intuition performs pattern recognition.

On the other hand, current theorem provers -- either with or without ML -- are quite weak compared to human provers, so I wouldn't try to prove the Jacobian conjecture with one.

I'm sorry because of adding another answer, but I can't undelete my message, and I do not arrive to talk to admins.

This domain is related to automated theorem proving. But as far as I know there is no automated theorem prover powerfull enough to create such a proof.

The actual automated theorem provers use propositional calculus or first order logic or second order logic to prove or refute theorems.

For instance if you would like to ask to an automated theorem prover if Jacobian Conjecture is true or false, you must ask a question like: is the theorem "commutative algebra and set theory and analysis implies jacobian conjecture" is true or false.

• In your earlier answer you cited a paper. Which one was that? – Jim May 16 '18 at 17:23
• Hi jim it was: "A fully automatic problem solver with human-style output" available on arxiv...it was related to automated theorem proving, but a part of the research about it, the part which try to imitate how the human reasoning works. I haven't yet read it all, but it seems it doesn't talk about machine learning – Nicolas Bourdon May 16 '18 at 19:59