Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2007P5

module

public import Mathlib.Tactic

public section


/-!
# USA Mathematical Olympiad 2007 P5
Prove that for every nonnegative integer n, the number 7^7^n + 1 is the product of at
least 2n + 3 (not necessarily distinct) primes.
-/

namespace USA2007P5
open Nat
theorem usa2007_p5 (n : ℕ) : 2*n + 3 ≤ (primeFactorsList (7^7^n+1)).length := sorry


end USA2007P5

File author(s): Pacmanboss256, hillosanation

This problem has a complete formalized solution.