Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1986P1

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Tactic.IntervalCases
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.NormNum.Prime

public section


/-!
# USA Mathematical Olympiad 1986, Problem 1

(a) Do there exist 14 consecutive positive integers, each of which is
divisible by a prime less than 13?

(b) Do there exist 21 consecutive positive integers, each of which is
divisible by a prime less than 17?
-/

namespace Usa1986P1

/- determine -/ abbrev does_exist_14 : Bool := sorry

/- determine -/ abbrev does_exist_21 : Bool := sorry

theorem usa1986_p1a :
    if does_exist_14 then
      ∃ n : ℕ, 0 < n ∧
        ∀ i ∈ Finset.range 14, ∃ p : ℕ, p.Prime ∧ p < 13 ∧ p ∣ n + i
    else
      ¬ ∃ n : ℕ, 0 < n ∧
        ∀ i ∈ Finset.range 14, ∃ p : ℕ, p.Prime ∧ p < 13 ∧ p ∣ n + i := sorry

theorem usa1986_p1b :
    if does_exist_21 then
      ∃ n : ℕ, 0 < n ∧
        ∀ i ∈ Finset.range 21, ∃ p : ℕ, p.Prime ∧ p < 17 ∧ p ∣ n + i
    else
      ¬ ∃ n : ℕ, 0 < n ∧
        ∀ i ∈ Finset.range 21, ∃ p : ℕ, p.Prime ∧ p < 17 ∧ p ∣ n + i := sorry

end Usa1986P1

File author(s): Kimi K3

This problem has a complete formalized solution.