Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2026P6

module

public import Mathlib.Tactic
public import Mathlib.Data.Nat.Totient
public import Mathlib.Data.Nat.Fib.Basic
public import Mathlib.Data.Nat.Factorization.PrimePow
public import Mathlib.Data.Nat.PrimeFin
public import Mathlib.Data.ZMod.Basic
public import Mathlib.FieldTheory.Finite.Basic
public import Mathlib.GroupTheory.OrderOfElement

public section


/-!
# USA Mathematical Olympiad 2026, Problem 6

Let a and b be positive integers such that φ(ab + 1) divides a² + b² + 1.
Prove that a and b are Fibonacci numbers.
-/

namespace Usa2026P6

theorem usa2026_p6 {a b : ℕ} (ha : 0 < a) (hb : 0 < b)
    (h : Nat.totient (a * b + 1) ∣ a ^ 2 + b ^ 2 + 1) :
    (∃ m, a = Nat.fib m) ∧ (∃ n, b = Nat.fib n) := sorry

end Usa2026P6

File author(s): Kimi K3

This problem has a complete formalized solution.