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