Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2001P5

module

public import Mathlib.RingTheory.Int.Basic

public section


/-!
# USA Mathematical Olympiad 2001, Problem 5

Let S be a set of integers (not necessarily positive) such that

(a) there exist a, b ∈ S with gcd(a, b) = gcd(a − 2, b − 2) = 1;
(b) if x and y are elements of S (possibly equal), then x² − y also belongs to S.

Prove that S is the set of all integers.
-/

namespace Usa2001P5

theorem usa2001_p5 (S : Set ℤ) (hS : ∀ x ∈ S, ∀ y ∈ S, x^2 - y ∈ S)
    (a b : ℤ) (ha : a ∈ S) (hb : b ∈ S)
    (h1 : Int.gcd a b = 1) (h2 : Int.gcd (a - 2) (b - 2) = 1) :
    S = Set.univ := sorry

File author(s): Kimi K3

This problem has a complete formalized solution.