Answers.Body: <p>There are programming languages that allow you to verify a proof by induction. For example, I used  <a href="https://coq.inria.fr/" rel="nofollow noreferrer">Coq</a>, but I'm sure there are also others.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-06-07T06:15:30.543Z
Answers.LastActivityDate: 2021-06-07T21:45:24.170Z
Answers.LastEditDate: 2021-06-07T21:45:24.170Z
Answers.UserDisplayName: IAmUser
Answers.Body: <p>It is possible for some classes of problems. For instance, <a href="https://www.wolframalpha.com/input/?i=Prove%20%20by%20induction%20sum%20of%20k%5E3%20from%201%20to%20n%20%3D%20%28n%28n%2B1%29%29%5E2%2F2" rel="nofollow noreferrer">WolframAlpha can generate an induction proof</a> to the problem posed in the question.</p>
  <p>According to the author of this proof generator, he built a library of pattern-matched proofs to generate the proofs. More details about his approach can be find in <a href="https://blog.wolfram.com/2016/07/14/behind-wolframalphas-mathematical-induction-based-proof-generator/" rel="nofollow noreferrer">his write-up about the problem</a>.</p>
  <p>Other alternative (thought not induction-based) for automatically verifying these kind of identities (in special, hypergeometric identities) is by using algorithms such as Zeilberger's method along with the HYPER algorithm, both described in the excellent book <a href="https://www2.math.upenn.edu/%7Ewilf/AeqB.html" rel="nofollow noreferrer">A=B</a>, currently available for free by one of its co-authors.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-06-07T03:19:25.973Z
Answers.LastActivityDate: 2021-06-07T03:19:25.973Z
Answers.UserDisplayName: shamisen
Body: <p>Can a computer solve the following problem, i.e. make a proof by induction? And why?</p>
  <blockquote>
  <p>Prove by <strong>induction</strong> that <span class="math-container">$$\sum_{k=1}^nk^3=\left(\frac{n(n+1)}{2}\right)^2, \, \, \, \forall n\in\mathbb N .$$</span></p>
  </blockquote>
  <p>I'm doing a Ph.D. in pure maths. I love coding when I wanna have some fun, but I've never got too far in this field. I say my background because maybe there's someone who wants to explain this in a more abstract language there's a chance that I will understand it.</p>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-08-09T10:48:12.873Z
Comments.Text: Are you looking for **any** technique that is able to prove that statement, i.e. you are not necessarily looking for a machine learning approach, right?
Comments.UserDisplayName: nbro
Tags: <math><proofs><automated-theorem-proving>
Title: Can a computer make a proof by induction?
UserDisplayName: DIEGO JAURE
ThreadText: # Can a computer make a proof by induction?
  
  (Asked by: username_0 on 2020-08-09)
  
  Can a computer solve the following problem, i.e. make a proof by induction? And why?
  
  > Prove by **induction** that $$\sum\_{k=1}^nk^3=\left(\frac{n(n+1)}{2}\right)^2, \, \, \, \forall n\in\mathbb N .$$
  
  I'm doing a Ph.D. in pure maths. I love coding when I wanna have some fun, but I've never got too far in this field. I say my background because maybe there's someone who wants to explain this in a more abstract language there's a chance that I will understand it.
  
  **Tags:** math, proofs, automated-theorem-proving
  > **Comments:**
  > **username_1**: Are you looking for **any** technique that is able to prove that statement, i.e. you are not necessarily looking for a machine learning approach, right?  
  
  ---
  
  ## 2 answers
  
  ### Answer by username_3 on 2021-06-07. Score: 2 | Accepted answer
  
  It is possible for some classes of problems. For instance, [WolframAlpha can generate an induction proof](https://www.wolframalpha.com/input/?i=Prove%20%20by%20induction%20sum%20of%20k%5E3%20from%201%20to%20n%20%3D%20%28n%28n%2B1%29%29%5E2%2F2) to the problem posed in the question.
  
  According to the author of this proof generator, he built a library of pattern-matched proofs to generate the proofs. More details about his approach can be find in [his write-up about the problem](https://blog.wolfram.com/2016/07/14/behind-wolframalphas-mathematical-induction-based-proof-generator/).
  
  Other alternative (thought not induction-based) for automatically verifying these kind of identities (in special, hypergeometric identities) is by using algorithms such as Zeilberger's method along with the HYPER algorithm, both described in the excellent book [A=B](https://www2.math.upenn.edu/%7Ewilf/AeqB.html), currently available for free by one of its co-authors.
  
  
  ---
  
  ### Answer by username_2 on 2021-06-07. Score: 3
  
  There are programming languages that allow you to verify a proof by induction. For example, I used [Coq](https://coq.inria.fr/), but I'm sure there are also others.
  
  
  ---
  
  