Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2017P1

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.ModEq
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Data.Set.Card
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Tactic.Ring

/-!
# USA Mathematical Olympiad 2017, Problem 1

Prove that there are infinitely many distinct pairs $(a,b)$ of
relatively prime positive integers $a>1$ and $b>1$ such that
$a^b+b^a$ is divisible by $a+b$.
-/

namespace Usa2017P1

def condition (a b : ℕ) : Prop :=
  Nat.gcd a b = 1 ∧ a > 1 ∧ b > 1 ∧ (a + b) ∣ (a ^ b + b ^ a)

theorem infinite_solution_set :
    Infinite { (x, y) : ℕ × ℕ | condition x y } := sorry

end Usa2017P1

File author(s): Elan Roth

This problem has a complete formalized solution.