Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1978P1

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1978, Problem 1

m and n are positive integers with m < n.
The last three decimal digits of 1978m are the same as the last three decimal digits of 1978n.
Find m and n such that m + n has the least possible value.
-/

namespace Imo1978P1

/- determine -/ abbrev solution : ℕ × ℕ := sorry

theorem imo1978_p1 (m n : ℕ)
  (hmn: m < n)
  (hmn2: (m, n) = solution) :
    (1978^m) % 1000 = (1978^n) % 1000 ∧
    (∀ m' n' : ℕ, m' < n' ∧ (1978^m') % 1000 = (1978^n') % 1000 → m + n ≤ m' + n') := sorry


end Imo1978P1

File author(s): InternLM-MATH LEAN Formalizer v0.1

This problem does not yet have a complete formalized solution.