Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1977P5

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1977, Problem 5

Let $a,b$ be two natural numbers. When we divide $a^2+b^2$ by $a+b$, we get the remainder $r$ and the quotient $q$. Determine all pairs $(a, b)$ for which $q^2 + r = 1977$.

-/

namespace Imo1977P5

/- determine -/ abbrev solution_set : Set (ℕ×ℕ) := sorry


theorem imo1977_p5
  (a b q r : ℕ)
  (hp: 0 < a ∧ 0 < b)
  (h₀ : r = (a ^ 2 + b ^ 2) % (a + b))
  (h₁ : q = (a ^ 2 + b ^ 2) / (a + b)) :
  q ^ 2 + r = 1977 ↔ (a, b) ∈ solution_set := sorry

File author(s): Roozbeh Yousefzadeh

This problem has a complete formalized solution.

The solution was imported from IMO-Steps/Lean_v20/imo_proofs/imo_1977_p5.lean.