Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1991P3

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.FieldTheory.Finite.Basic

public section


/-!
# USA Mathematical Olympiad 1991, Problem 3

Define the function $f$ on the natural numbers by $f(1) = 2$, $f(n) = 2^{f(n-1)}$.
Show that $f(n)$ has the same residue mod $m$ for all sufficiently large $n$.
-/

namespace Usa1991P3

/-- The tower-of-exponents function of the problem, with the index shifted by one:
`f 0 = 2` and `f (n + 1) = 2 ^ f n`, so that the problem's `f n` is our `f (n - 1)`. -/
def f : ℕ → ℕ
  | 0 => 2
  | n + 1 => 2 ^ f n

theorem usa1991_p3 (m : ℕ) (hm : 1 ≤ m) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → f n ≡ f N [MOD m] := sorry

end Usa1991P3

File author(s): Kimi K3

This problem has a complete formalized solution.