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?  
 A: 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.
A: 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.
