Building an Automated Theorem Prover with Machine Learning

Question

I am very interested in developing a machine-learning algorithm that could learn from the axioms, properties of the mathematical system of interest, and positive examples from the conjecture of interest to infer some key properties of the possible proof to the conjecture. Such interest led me to the art of automated theorem prover, which seems to exist more than I know.

Is ATP applicable to the fields in algebraic geometry and set-theoretic topology? I am very interested in trying to prove Jacobian Conjecture, which is related to the computation learning theory. I am lost in the sea of ATP, so I am curious if you could suggest me some books and articles that describe ATP. I am also curious how applicable is ATP to the algebraic geometry.

Answer 1

This surely sounds like an interesting thought. But most machine learning methods, as it stands today, are used for classification/regression type problems. More recently (meaning a few years ago) due to the growth of computing machinery and libraries they have been adapted for strategy selection in games and other systems like self driving cars. All the same, if you want a list of good books to learn probability theory here is a good list to choose from.

Answer 2

For an introduction to automated theorem proving:

• Handbook of Practical Logic and Automated Reasoning, by John Harrison.
• Handbook of Automated Reasoning, edited by Alan Robinson and Andrei Voronkov.

About the use of machine learning for ATP, you can read the papers of Josef Urban and Cezary Kaliszyk : https://scholar.google.com/citations?user=4pW-Je4AAAAJ&hl=en

Automated Theorem Proving is very successful in 'elementary' geometry, there are methods which can solve hundreds of non trivial theorems: Wu's method, Gröbner basis, the area method,... Chapter 11 of Handbook of Automated Reasoning - Automated Reasoning in Geometry, Pages 707, 709-749, Shang-Ching Chou, Xiao-Shan Gao, provides an overview of the methods.

But, I am not aware of any method for automated reasoning in geometry which could be used for proving the Jacobian conjecture.