How to prove an expression by method of mathematical induction?

Question

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?

Answer 1

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

Answer 2

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)

Answer 3

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}