8
$\begingroup$

I want to prove the expression $$1^2 + 2^2 + 3^2 + \cdots + n^2 = \dfrac{n(n+1)(2n+1)}{6}$$ by method of mathematical induction with Mathematica, but I do not know how to start. How do I tell Mathematica to do that?

$\endgroup$
2
  • $\begingroup$ You're not satisfied with Sum[k^2, {k, n}] // Factor generating the expression you want? $\endgroup$ Oct 19, 2012 at 15:10
  • $\begingroup$ I want to prove that step - by - step. $\endgroup$ Oct 19, 2012 at 15:14

4 Answers 4

17
$\begingroup$
f[n_] := (n (n + 1) (2 n + 1))/6

Easy. The proof by induction involves two steps:

  1. Prove the relation for a starting value. We'll take n=1. So f[1] must equal 1^2:

    f[1] == 1
    

    True

  2. Prove that, if the relation holds for a certain n, it also holds for n+1. In this case, for n+1 we have to add (n+1)^2 to the sum you get for n:

    f[n] + (n + 1)^2 == f[n + 1]// FullSimplify
    

    True

$\endgroup$
3
  • 1
    $\begingroup$ The "inductive step" #2, as shown, sort of begs the question in that by hand you've done the principal work already, namely, representing $\sum_{j=1}^{n+1} j^2$ as $\sum_{j=1}^n j^2 + (n+1)^2$. That's pretty obvious a thing to do for the case at hand, but in general the inductive step in a proof by induction is not so obvious to carry out. All you've done here is use Mathematica to carry out the (fairly trivial) algebraic simplification to complete the inductive step. It's hardly what I would deem to be an actual inductive proof. $\endgroup$
    – murray
    Oct 24, 2012 at 16:18
  • 1
    $\begingroup$ @Murray I'm sorry that you don't like it. What would you suggest here? $\endgroup$ Oct 24, 2012 at 17:44
  • $\begingroup$ C. deVries: I'm suggesting that one cannot really use Mathematica to do an inductive proof! Perhaps with an add-on such as Theorema (once it's updated to current Mathematica versions). $\endgroup$
    – murray
    Oct 24, 2012 at 21:26
9
$\begingroup$

Induction has many faces, a straightforward way to prove the equality using induction is

1. RSolve

It is superior because we needn't know the formula. Denote s[n] to be the sum 1^2 + 2^2 +...+ n^2 for every natural n, then obviously the axiom of induction is equivalent to : s[n+1] - s[n] == (n+1)^2, and the initial condition is : s[0] == 0, thus :

RSolve[{s[n + 1] - s[n] == (n + 1)^2, s[0] == 0}, s[n], n] // Factor
{{s[n] -> 1/6 n (1 + n) (1 + 2 n)}}

we have proved the equality.

Alternatively we could use

2. FindSequenceFunction

giving a few successive sums 1^2 + 2^2 +...+ n^2, it appears we need the first 5 sums :

FindSequenceFunction[{1, 5, 14, 30, 55}, n] // Factor
1/6 n (1 + n) (1 + 2 n)

Another the most obvious way using induction more or less implicitly is

3. Sum

for a general natural n we have :

Sum[ k^2, {k, n}]
1/6 n (1 + n) (1 + 2 n)

One can find an indetermined sum as well, but then the index starts at 0, therfore one needs to substitute n -> n+1 implying , e.g :

Sum[n^2, n] /. n -> n + 1 // Simplify
1/6 n (1 + n) (1 + 2 n)
$\endgroup$
2
$\begingroup$

This is another way which I have just found. Prove the expression $$1 + 2 + \cdots + n = \dfrac{n(n+1)}{2}.$$

prL[n_] := Sum[i, {i, 1, n}] // HoldForm; prR[n_] := 1/2*n*(n + 1);
{eq1 = ReleaseHold[prL[1]] == prR[1], eq2 = prL[k] == prR[k], 
 eq3 = prL[k] + (k + 1) == prR[k] + (k + 1), 
 eq4 = prL[k + 1] == Factor[eq3[[2]]], 
 eq5 = eq4 /. {k + 1 -> n, 2 + k -> n + 1}, 
 eq6 = (eq2 /. {k -> n}) === eq5}
$\endgroup$
2
  • 3
    $\begingroup$ Isn't this more like writing out a pencil and paper proof in Mathematica? $\endgroup$
    – rm -rf
    Oct 19, 2012 at 16:17
  • 1
    $\begingroup$ @rm-rf Perhaps that's the idea? Electronic paper with Mathematica checking your figures? $\endgroup$
    – Mr.Wizard
    Oct 19, 2012 at 17:48
2
$\begingroup$

just to clarify @Sjoerd C. de Vries answer

  1. we specify the sequence to solve/proof:

    element[i_]:=i^2
    s[n_] := Sum[elemen[i], {i,n}]
    
  2. we guess the solution:

    f[n_] := (n (n + 1) (2 n + 1))/6
    
  3. we proof an initial point n0:

    n0=1;
    f[n0]
    

    1

    s[n0]
    

    1

    f[n0] == s[n0]
    

    True

  4. we check the guess for n+1: we do this by adding(*) the (n+1)th element to f[n] and compare/equal with f[n+1]

    (*) in this case we add because we deal with a sum and adding gets us the next element of a sum

    {element[n + 1] + f[n], f[n + 1]}
    

    {(1 + n)^2 + 1/6 n (1 + n) (1 + 2 n), 1/6 (1 + n) (2 + n) (1 + 2 (1 + n))}

    % // Expand
    

    {1 + (13 n)/6 + (3 n^2)/2 + n^3/3, 1 + (13 n)/6 + (3 n^2)/2 + n^3/3}

    % // Apply@Equal
    

    True

This proofs that if the guess ist correct for an arbitrary n it is also correct for n+1. Together with the correctness for the initial point n0 we now have proved the correctness for all n: n0 <= n < ∞

$\endgroup$

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.