Fermat numbers

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-08-26.
Last modified on 2024-10-24.

module elementary-number-theory.fermat-numbers where
Imports 
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.exponentiation-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.products-of-natural-numbers
open import elementary-number-theory.strong-induction-natural-numbers

open import univalent-combinatorics.standard-finite-types

Idea

Fermat numbers are numbers of the form . The first five Fermat numbers are

  3, 5, 17, 257, and 65537.

The sequence of Fermat numbers is listed as A000215 in the Online Encyclopedia of Integer Sequences.

Alternatively, the Fermat numbers can be defined with strong induction by

F 0 := 3
F (n + 1) := 2 + Π_{i≤n} F_i

This recurrence implies that any two Fermat numbers are relatively prime. Goldbach used this observation to prove the infinitude of primes: Since there are infinitely many Fermat numbers, and all of them are relatively prime, there must be infinitely many prime numbers. Fermat numbers also feature in a series of long-standing open problems in mathematics, including:

  • Are there infinitely many prime Fermat numbers?
  • Is composite for all ?

Definition

The Fermat numbers

fermat-number-ℕ : ℕ → ℕ
fermat-number-ℕ n = exp-ℕ 2 (exp-ℕ 2 n) +ℕ 1

The recursive definition of the Fermat numbers

recursive-fermat-number-ℕ : ℕ → ℕ
recursive-fermat-number-ℕ =
  strong-rec-ℕ 3
    ( λ n f →
      add-ℕ
        ( Π-ℕ
          ( succ-ℕ n)
          ( λ i → f (nat-Fin (succ-ℕ n) i) (upper-bound-nat-Fin n i)))
        ( 2))

Recent changes