9
$\begingroup$

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?

Improve this question
$\endgroup$
5
  • $\begingroup$ I'd like to link Q: machine learning applications in number theory. It asks something similar specifically for Number Theory. $\endgroup$
    – Jim
    Commented May 15, 2018 at 16:47
  • $\begingroup$ 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. $\endgroup$
    – Tim
    Commented May 15, 2018 at 19:52
  • 2
    $\begingroup$ 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). $\endgroup$
    – Mark L. Stone
    Commented May 15, 2018 at 20:23
  • 1
    $\begingroup$ Related: Is it possible to train the neural network to solve math equations? $\endgroup$
    – kenorb
    Commented Nov 30, 2018 at 13:33
  • $\begingroup$ See also: mathoverflow.net/q/390174/2312 on applications of deep learning to research mathematics $\endgroup$
    – J W
    Commented Apr 16, 2021 at 6:18

2 Answers 2

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$
0
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ In your earlier answer you cited a paper. Which one was that? $\endgroup$
    – Jim
    Commented May 16, 2018 at 17:23
  • $\begingroup$ 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 $\endgroup$
    – Nicolas Bourdon
    Commented May 16, 2018 at 19:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.