Term is over and I have spent the entire day thinking about induction. I was mainly concerned about the fact that induction somehow seemed hard for mathematicians to do in Lean. Even proving that the sum of the first `n`

odd positive integers was `n^2`

seemed to be complicated. But I now know several ways of doing it, and I want to see if I can guide you to coming up with one yourself. Note that I think these Lean exercises are hard for mathematicians, because unfortunately mathematicians (correctly in my opinion) would regard the statement that the sum of the first odd positive integers was as “trivial by induction”. Let me try and show you several ways of doing induction in Lean. Not because I want to know several ways to do it, but, unfortunately, because I fear that in practice people really might occasionally find themselves in a situation where they need a new kind of proof by induction, and if they read this then maybe afterwards they’ll understand the exact statements that they need to prove to get induction working.

This entire exercise is available for the Lean Web Editor by the way. It’s also available in the Xena project (in the blog directory) if you want to download it to run in a local copy of Lean (which is highly recommended).

OK so let’s start with the two functions in our induction proof:

```
def odd : ℕ → ℕ := λ i, 2 * i + 1
def square : ℕ → ℕ := λ i, i ^ 2
```

You can play around with them, check by typing `#reduce odd 2`

and you can check that by typing `#eval square 1000`

(for extra credit: what happens if you type `#reduce square 1000`

? Why?). It’s well-known that the sum of the first positive odd integers is and it’s well-known that one can prove it by induction, with the key inductive step being that . We can formalize this neatly in Lean:

```
theorem odd_square_inductive_step (d : ℕ) : square d + odd d = square (succ d)
```

and one can prove it relatively easily, using the `ring`

tactic, as one can see in the downloadable file.

What is left is the question on how we are going to write the function which takes as input and writes down the sum . Then everything should be straightforward. But there are several ways to define this function!

**Exercise 1.**

Define a Lean function which takes as input a function `f : ℕ → ℕ`

and returns the function which sends a natural number n to .

```
definition my_sum_to_n (summand : ℕ → ℕ) : ℕ → ℕ :=
sorry -- delete this and then fill in your definition here.
```

**Exercise 2.**

The function you defined comes with a law of induction, and you now need to prove the zero and successor results for your function.

```
theorem my_zero_theorem (summand : ℕ → ℕ) : my_sum_to_n summand 0 = 0 := sorry
theorem my_successor_theorem (summand : ℕ → ℕ) (n : ℕ) :
my_sum_to_n summand (nat.succ n) = my_sum_to_n summand n + summand n := sorry
```

**Exercise 3**

Now can you prove my_odd_square_theorem, the fact that the sum of the first odd positive integers is ?

```
theorem my_odd_square_theorem (n : ℕ) : my_sum_to_n odd n = square n := sorry
```

**Exercise 4**

Finally, find someone who has given a completely different definition of `my_sum_to_n`

(try looking in the comments below, for example) and

add their definition to your session (to your “context”):

```
definition other_sum_to_n (summand : ℕ → ℕ) : ℕ → ℕ := sorry
```

and now see if you can prove that their definition is the same as yours.

```
theorem consistency : my_sum_to_n = other_sum_to_n := sorry
```

[You might want to start

`begin apply funext,intro f,apply funext,intro n,`

…]

I will give some possible definitions for `my_sum_to_n`

in the comments, if nobody else gets there first.