# How to prove an expression by method of mathematical induction?

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?

• You're not satisfied with Sum[k^2, {k, n}] // Factor generating the expression you want? – J. M. is in limbo Oct 19 '12 at 15:10
• I want to prove that step - by - step. – minthao_2011 Oct 19 '12 at 15:14

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 must equal 1^2:

f == 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

• 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. – murray Oct 24 '12 at 16:18
• @Murray I'm sorry that you don't like it. What would you suggest here? – Sjoerd C. de Vries Oct 24 '12 at 17:44
• 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). – murray Oct 24 '12 at 21:26

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, thus :

RSolve[{s[n + 1] - s[n] == (n + 1)^2, s == 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)


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] == prR, eq2 = prL[k] == prR[k],
eq3 = prL[k] + (k + 1) == prR[k] + (k + 1),
eq4 = prL[k + 1] == Factor[eq3[]],
eq5 = eq4 /. {k + 1 -> n, 2 + k -> n + 1},
eq6 = (eq2 /. {k -> n}) === eq5}

• Isn't this more like writing out a pencil and paper proof in Mathematica? – rm -rf Oct 19 '12 at 16:17
• @rm-rf Perhaps that's the idea? Electronic paper with Mathematica checking your figures? – Mr.Wizard Oct 19 '12 at 17:48

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 < ∞