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?

Improve this question
$\endgroup$
2
  • $\begingroup$ You're not satisfied with Sum[k^2, {k, n}] // Factor generating the expression you want? $\endgroup$
    – J. M.'s missing motivation ♦
    Commented Oct 19, 2012 at 15:10
  • $\begingroup$ I want to prove that step - by - step. $\endgroup$
    – minthao_2011
    Commented Oct 19, 2012 at 15:14

4 Answers 4

Reset to default
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

Improve this answer
$\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
    Commented Oct 24, 2012 at 16:18
  • 1
    $\begingroup$ @Murray I'm sorry that you don't like it. What would you suggest here? $\endgroup$
    – Sjoerd C. de Vries
    Commented 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
    Commented 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)
Improve this answer
$\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}
Improve this answer
$\endgroup$
2
  • 3
    $\begingroup$ Isn't this more like writing out a pencil and paper proof in Mathematica? $\endgroup$
    – rm -rf ♦
    Commented 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
    Commented 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 < ∞

Improve this answer
$\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.