Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2014P6

module

public import Mathlib.Algebra.BigOperators.Associated
public import Mathlib.Algebra.CharP.Defs
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Data.Nat.Cast.Order.Field
public import Mathlib.Data.Nat.Factorization.Basic
public import Mathlib.Data.Nat.Log
public import Mathlib.Data.Rat.Star
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Positivity.Basic
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 2014, Problem 6

Prove that there is a constant c > 0 with the following property:
If a, b, n are positive integers such that gcd(a + i, b + j) > 1
for all i, j ∈ {0, 1, ..., n}, then min{a, b} > (cn)ⁿ.
-/

namespace Usa2014P6

open Finset

theorem usa2014_p6 :
    ∃ c : ℝ, 0 < c ∧
      ∀ a b n : ℕ, 0 < a → 0 < b → 0 < n →
        (∀ i ∈ range (n + 1), ∀ j ∈ range (n + 1), 1 < Nat.gcd (a + i) (b + j)) →
        (c * (n : ℝ)) ^ n < ((min a b : ℕ) : ℝ) := sorry

end Usa2014P6

File author(s): Kimi K3

This problem has a complete formalized solution.