Answers.Body: <p>Not in such straight forward way as described, but neural networks are successfully applied to guide the search of proof. There are automated theorem provers. What they do look roughly like this:</p>
  
  <ol>
  <li><p>Get the mathematical statement</p></li>
  <li><p>Apply one of the known mathematical equivalence transformations (theorems, axioms, etc)</p></li>
  <li><p>Check, if the resulting statement is trivially true. Then our sequence of transformations is the proof (since they all were equivalence transformations). Else, goto 2.</p></li>
  </ol>
  
  <p>The tricky part here is to choose which transformation to apply at step 2. A neural network can be trained to predict function like</p>
  
  <blockquote>
    <p>Statement, Transformation --> usefulness of that transformation to that statement</p>
  </blockquote>
  
  <p>Then, during the search, we can apply such transformation, that neural network considers the most useful. Also, proving a theorem can be considered game, where axioms are the rules, and when you've reached the proof you win. In this form, Reinforcement Learning agents can be applied to prove theorems (this is also successfully done).</p>
  
  <p>Here are papers that do similar things: </p>
  
  <ul>
  <li><p><a href="https://arxiv.org/pdf/1907.07794.pdf" rel="noreferrer">Generating Correctness Proofs with Neural Networks</a> (<a href="https://github.com/UCSD-PL/proverbot9001" rel="noreferrer">Proverbot9001</a>)</p></li>
  <li><p><a href="https://arxiv.org/pdf/1806.00608.pdf" rel="noreferrer">A Learning Environment for Theorem Proving</a> (<a href="https://github.com/ml4tp/gamepad" rel="noreferrer">GamePad</a>)</p></li>
  <li><p><a href="https://arxiv.org/pdf/1804.00596.pdf" rel="noreferrer">Learning to Prove with Tactics</a> (TacticToe)</p></li>
  <li><p><a href="https://arxiv.org/pdf/1905.09381.pdf" rel="noreferrer">Learning to Prove Theorems via Interacting with Proof Assistants</a> (<a href="https://github.com/princeton-vl/CoqGym" rel="noreferrer">CoqGym</a>)</p></li>
  <li><p><a href="http://proceedings.mlr.press/v97/bansal19a/bansal19a.pdf" rel="noreferrer">HOList: An Environment for Machine Learning of Higher-Order Theorem Proving</a></p></li>
  <li><p><a href="https://papers.nips.cc/paper/8098-reinforcement-learning-of-theorem-proving.pdf" rel="noreferrer">Reinforcement Learning of Theorem Proving</a> (rlCoP)</p></li>
  </ul>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-04-19T18:10:38.073Z
Answers.LastActivityDate: 2020-04-20T20:17:17.637Z
Answers.LastEditDate: 2020-04-20T20:17:17.637Z
Answers.UserDisplayName: Arqwer
Answers.Body: <p>It's possible, but probably not a good idea.</p>
  
  <p>Logical proof is one of the oldest areas of AI, and there are purpose-built techniques that don't need to be trained, and that are more reliable than a neural-network approach would be, since they don't rely on statistical reasoning, and instead use the mathematician's friend: deductive reasoning.</p>
  
  <p>The main field is called "<a href="https://en.wikipedia.org/wiki/Automated_theorem_proving" rel="noreferrer">Automated Theorem Proving</a>", and it's old enough that it's calcified a bit as a research area. There are not a lot of innovations, but some people still work on it.</p>
  
  <p>The basic idea is that theorem proving is just classical or heuristic guided search: you start from a state consisting of a set of accepted premises. Then you apply any valid logical rule of inference to generate new premises that must also be true, expanding the set of knowledge that you have. Eventually, you can prove a desired premise, either through enumerative searches like <a href="https://en.wikipedia.org/wiki/Breadth-first_search" rel="noreferrer">breadth first search</a> or <a href="https://en.wikipedia.org/wiki/Iterative_deepening_depth-first_search" rel="noreferrer">iterative deepening</a>, or through something like <a href="https://en.wikipedia.org/wiki/A*_search_algorithm" rel="noreferrer">A*</a> with a domain-specific heuristic. A lot of solvers also use just one logical rule (<a href="https://en.wikipedia.org/wiki/Unification_(computer_science)" rel="noreferrer">unification</a>) because it's complete, and reduces the branching factor of the search.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2018-08-04T15:00:06.637Z
Answers.LastActivityDate: 2018-08-04T15:08:39.773Z
Answers.LastEditDate: 2018-08-04T15:08:39.773Z
Answers.UserDisplayName: John Doucette
Answers.Body: <p>Your idea may be feasible in general, but a neural network is probably the wrong <em>high level</em> tool to use to explore this problem.</p>
  
  <p>A neural network's strength is in finding internal representations that allow for a highly nonlinear solution when mapping inputs to outputs. When we train a neural network, those mappings are learned statistically through repetition of examples. This tends to produce models that <em>interpolate</em> well when given data similar to training set, but that <em>extrapolate</em> badly. </p>
  
  <p>Neural network models also lack context, such that if you used a generative model (e.g. an RNN trained on sequences that create valid or interesting proof) then it can easily produce statistically pleasing but meaningless rubbish. </p>
  
  <p>What you will need is some organising principle that allows you to explore and confirm proofs in a combinatorial fashion. In fact something like your idea has already been done more than once, but I am not able to find a reference currently.</p>
  
  <p>None of this stops you using a neural network within an AI that searches for proofs. There may be places within a maths AI where you need a good heuristic to guide searches for instance - e.g. in context X is sub-proof Y likely to be interesting or relevant. Assessing a likelihood score <em>is</em> something that a neural network can do as part of a broader AI scheme. That's similar to how neural networks are combined with reinforcement learning.</p>
  
  <p>It may be possible to build your idea entirety out of neural networks in principle. After all, there are good reasons to suspect human reasoning works similarly using biological neurons (not proven that artificial ones can match this either way). However, the architecture of such a system is beyond any modern NN design or training setup. It definitely will not be a matter of just adding enough layers then feeding in data.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2018-08-04T15:03:26.880Z
Answers.LastActivityDate: 2018-08-04T15:03:26.880Z
Answers.UserDisplayName: Neil Slater
Answers.Body: <p>I've published an article with the corresponding new method based on the generative grammars of first-order theories:</p>
  <p><a href="https://www.academia.edu/43984841/Thoughts_on_generative_grammars_and_their_use_in_automated_theorem_proving_based_on_neural_networks_with_a_type_0_grammar_of_Nicods_propositional_logic_system_added_" rel="nofollow noreferrer">Thoughts on generative grammars and their use in automated theorem proving based on neural networks</a></p>
  <p>This approach allows not to use previous data but to generate it as much as it's needed in machine learning. In the article, you may find necessary theory on logic, grammars, and neural networks. You'll also find examples of the python-functions generating proofs literally. I've added a grammar for the propositional logic that can be naturally enlarged to the &quot;real&quot; cases of first-order theories (say, group or number theory).</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-09-04T19:16:24.257Z
Answers.Text: I suggest that you provide a link to the pdf that we can access freely. I am not familiar with that site, but to access your article I need to log-in with google or facebook.
Answers.UserDisplayName: nbro
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-08-31T21:08:37.917Z
Answers.LastActivityDate: 2020-09-02T21:36:32.653Z
Answers.LastEditDate: 2020-09-02T21:36:32.653Z
Answers.UserDisplayName: Rebel Yell
Body: <p>Imagine I have a list (in a computer-readable form) of all problems (or statements) and proofs that math relies on. </p>
  
  <p>Could I train a neural network in such a way that, for example, I enter a problem and it generates a proof for it?</p>
  
  <p>Of course, those proofs then needed to be checked manually, but maybe the network then creates proofs from combinations of older proofs for problems yet unsolved.</p>
  
  <p>Is that possible?</p>
  
  <p>Would it be possible, for example, to solve the Collatz-conjecture or the Riemann-conjecture with this type of network? Or, if not solve, but maybe rearrange patterns in a way that mathematicians are able to use a new "proof method" to make a real proof?</p>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-09-01T13:10:23.860Z
Comments.Text: You will anyway be confronted with [Gödel's incompleteness theorem](https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems), which is mathematically proven, and says in a nutshell that some conjectures are true _but_ not provable. So we know for sure that there is no universal theorem-prover.
Comments.UserDisplayName: Pierre Gramme
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2021-01-21T22:41:13.047Z
Comments.Text: [Here](https://ai.stackexchange.com/q/154/2444) is a related question.
Comments.UserDisplayName: nbro
Tags: <neural-networks><math><automated-theorem-proving>
Title: Can neural networks be used to prove conjectures?
UserDisplayName: Max Mustermann Junior
ThreadText: # Can neural networks be used to prove conjectures?
  
  (Asked by: username_0 on 2018-08-04)
  
  Imagine I have a list (in a computer-readable form) of all problems (or statements) and proofs that math relies on.
  
  Could I train a neural network in such a way that, for example, I enter a problem and it generates a proof for it?
  
  Of course, those proofs then needed to be checked manually, but maybe the network then creates proofs from combinations of older proofs for problems yet unsolved.
  
  Is that possible?
  
  Would it be possible, for example, to solve the Collatz-conjecture or the Riemann-conjecture with this type of network? Or, if not solve, but maybe rearrange patterns in a way that mathematicians are able to use a new "proof method" to make a real proof?
  
  **Tags:** neural-networks, math, automated-theorem-proving
  
  > **Comments:**
  > **username_1**: You will anyway be confronted with [Gödel's incompleteness theorem](https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems), which is mathematically proven, and says in a nutshell that some conjectures are true _but_ not provable. So we know for sure that there is no universal theorem-prover.  
  > **username_2**: [Here](https://ai.stackexchange.com/q/154/2444) is a related question.  
  
  ---
  
  ## 4 answers
  
  ### Answer by username_3 on 2020-04-19. Score: 9
  
  Not in such straight forward way as described, but neural networks are successfully applied to guide the search of proof. There are automated theorem provers. What they do look roughly like this:
  
  1. Get the mathematical statement
  2. Apply one of the known mathematical equivalence transformations (theorems, axioms, etc)
  3. Check, if the resulting statement is trivially true. Then our sequence of transformations is the proof (since they all were equivalence transformations). Else, goto 2.
  
  The tricky part here is to choose which transformation to apply at step 2. A neural network can be trained to predict function like
  
  > Statement, Transformation --> usefulness of that transformation to that statement
  
  Then, during the search, we can apply such transformation, that neural network considers the most useful. Also, proving a theorem can be considered game, where axioms are the rules, and when you've reached the proof you win. In this form, Reinforcement Learning agents can be applied to prove theorems (this is also successfully done).
  
  Here are papers that do similar things:
  
  * [Generating Correctness Proofs with Neural Networks](https://arxiv.org/pdf/1907.07794.pdf) ([Proverbot9001](https://github.com/UCSD-PL/proverbot9001))
  * [A Learning Environment for Theorem Proving](https://arxiv.org/pdf/1806.00608.pdf) ([GamePad](https://github.com/ml4tp/gamepad))
  * [Learning to Prove with Tactics](https://arxiv.org/pdf/1804.00596.pdf) (TacticToe)
  * [Learning to Prove Theorems via Interacting with Proof Assistants](https://arxiv.org/pdf/1905.09381.pdf) ([CoqGym](https://github.com/princeton-vl/CoqGym))
  * [HOList: An Environment for Machine Learning of Higher-Order Theorem Proving](http://proceedings.mlr.press/v97/bansal19a/bansal19a.pdf)
  * [Reinforcement Learning of Theorem Proving](https://papers.nips.cc/paper/8098-reinforcement-learning-of-theorem-proving.pdf) (rlCoP)
  
  
  ---
  
  ### Answer by username_5 on 2018-08-04. Score: 8
  
  Your idea may be feasible in general, but a neural network is probably the wrong *high level* tool to use to explore this problem.
  
  A neural network's strength is in finding internal representations that allow for a highly nonlinear solution when mapping inputs to outputs. When we train a neural network, those mappings are learned statistically through repetition of examples. This tends to produce models that *interpolate* well when given data similar to training set, but that *extrapolate* badly.
  
  Neural network models also lack context, such that if you used a generative model (e.g. an RNN trained on sequences that create valid or interesting proof) then it can easily produce statistically pleasing but meaningless rubbish.
  
  What you will need is some organising principle that allows you to explore and confirm proofs in a combinatorial fashion. In fact something like your idea has already been done more than once, but I am not able to find a reference currently.
  
  None of this stops you using a neural network within an AI that searches for proofs. There may be places within a maths AI where you need a good heuristic to guide searches for instance - e.g. in context X is sub-proof Y likely to be interesting or relevant. Assessing a likelihood score *is* something that a neural network can do as part of a broader AI scheme. That's similar to how neural networks are combined with reinforcement learning.
  
  It may be possible to build your idea entirety out of neural networks in principle. After all, there are good reasons to suspect human reasoning works similarly using biological neurons (not proven that artificial ones can match this either way). However, the architecture of such a system is beyond any modern NN design or training setup. It definitely will not be a matter of just adding enough layers then feeding in data.
  
  
  ---
  
  ### Answer by username_4 on 2018-08-04. Score: 6
  
  It's possible, but probably not a good idea.
  
  Logical proof is one of the oldest areas of AI, and there are purpose-built techniques that don't need to be trained, and that are more reliable than a neural-network approach would be, since they don't rely on statistical reasoning, and instead use the mathematician's friend: deductive reasoning.
  
  The main field is called "[Automated Theorem Proving](https://en.wikipedia.org/wiki/Automated_theorem_proving)", and it's old enough that it's calcified a bit as a research area. There are not a lot of innovations, but some people still work on it.
  
  The basic idea is that theorem proving is just classical or heuristic guided search: you start from a state consisting of a set of accepted premises. Then you apply any valid logical rule of inference to generate new premises that must also be true, expanding the set of knowledge that you have. Eventually, you can prove a desired premise, either through enumerative searches like [breadth first search](https://en.wikipedia.org/wiki/Breadth-first_search) or [iterative deepening](https://en.wikipedia.org/wiki/Iterative_deepening_depth-first_search), or through something like [A\*](https://en.wikipedia.org/wiki/A*_search_algorithm) with a domain-specific heuristic. A lot of solvers also use just one logical rule ([unification](https://en.wikipedia.org/wiki/Unification_(computer_science))) because it's complete, and reduces the branching factor of the search.
  
  
  ---
  
  ### Answer by username_6 on 2020-08-31. Score: 1
  
  I've published an article with the corresponding new method based on the generative grammars of first-order theories:
  
  [Thoughts on generative grammars and their use in automated theorem proving based on neural networks](https://www.academia.edu/43984841/Thoughts_on_generative_grammars_and_their_use_in_automated_theorem_proving_based_on_neural_networks_with_a_type_0_grammar_of_Nicods_propositional_logic_system_added_)
  
  This approach allows not to use previous data but to generate it as much as it's needed in machine learning. In the article, you may find necessary theory on logic, grammars, and neural networks. You'll also find examples of the python-functions generating proofs literally. I've added a grammar for the propositional logic that can be naturally enlarged to the "real" cases of first-order theories (say, group or number theory).
  
  > **Comments:**
  > **username_2**: I suggest that you provide a link to the pdf that we can access freely. I am not familiar with that site, but to access your article I need to log-in with google or facebook.  
  
  ---
  
  