# Zulip Chat Archive

## Stream: new members

### Topic: recurrence on fermat numbers

#### Peter Ross (Jan 03 2022 at 20:16):

Hello I am new to Lean, and I would like help with proving a recurrence on the fermat numbers, which in latex is

```
\prod_{k=0}^{n-1} F_k = F_n-2
```

I tried to write it in Lean as

```
-- define a fermat number
def fermat_number (p : ℕ ) := 2^2^p +1
-- prove the recurrence on the Fermat numbers
lemma fermat_recurrence (n: ℕ ) : ∏ fermat_number x in range(n-1) = fermat_number n - 2 := begin
sorry,
end
```

but the error said "unexpected token". I don't know how to solve this because I am new to using Lean, so I would appreciate it if anyone would help me.

#### Ruben Van de Velde (Jan 03 2022 at 20:18):

You're looking for something more like `∏ x in range(n-1), fermat_number x = fermat_number n - 2`

#### Eric Rodriguez (Jan 03 2022 at 20:18):

you'll want `open_locale big_operators`

too

#### Yaël Dillies (Jan 03 2022 at 20:19):

And `range n`

instead of `range (n - 1)`

most likely.

#### Eric Rodriguez (Jan 03 2022 at 20:20):

(natural number subtraction is annoying in Lean)

#### Ruben Van de Velde (Jan 03 2022 at 20:23):

```
import tactic
open_locale big_operators
-- define a fermat number
def fermat_number (p : ℕ) := 2^2^p +1
-- prove the recurrence on the Fermat numbers
lemma fermat_recurrence (n: ℕ) : ∏ x in finset.range n, fermat_number x = fermat_number n - 2 :=
begin
sorry,
end
```

#### Stuart Presnell (Jan 03 2022 at 20:26):

To avoid the subtraction would it be better to write this?

```
lemma fermat_recurrence (n: ℕ) : ∏ x in finset.range (n+2), fermat_number x = fermat_number n :=
begin
sorry,
end
```

#### Kevin Buzzard (Jan 03 2022 at 20:28):

Nonono, the brackets aren't there. It's (fermat_number n) +2

#### Kevin Buzzard (Jan 03 2022 at 20:29):

The formalisation is fine with the subtraction because the Fermat numbers are all >= 3.

#### Kevin Buzzard (Jan 03 2022 at 20:31):

I think that the correct way to avoid nat subtraction is not to use nat:

```
import tactic
open_locale big_operators
-- define a Fermat number as an integer
def fermat_number (p : ℕ) := (2 : ℤ) ^ 2 ^ p + 1
open finset
-- prove the recurrence on the Fermat numbers
lemma fermat_recurrence (n: ℕ) : ∏ x in range n, fermat_number x = fermat_number n - 2 :=
begin
sorry,
end
```

#### Ruben Van de Velde (Jan 03 2022 at 20:31):

It appears to be true in lean:

#### Kevin Buzzard (Jan 03 2022 at 20:35):

The proof is simpler if you use integers.

#### Ruben Van de Velde (Jan 03 2022 at 20:35):

Isn't it always :)

#### Kevin Buzzard (Jan 03 2022 at 20:36):

Furthermore I would argue that the *moment* you use subtraction you're saying "I am assuming subtraction makes sense hence I am assuming these things are integers". I would argue that the integer version is a more correct way of translating into Lean the meaning of the original question, as well as being easier to work with.

Last updated: Dec 20 2023 at 11:08 UTC