Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1959P1

import Mathlib.Algebra.Divisibility.Basic
import Mathlib.Tactic.Ring
import Mathlib.Data.Nat.Prime.Basic

/-!
# International Mathematical Olympiad 1959, Problem 1.

Prove that the fraction `(21n+4)/(14n+3)` is irreducible for every
natural number `n`.
-/

namespace Imo1959P1

/-
Since Lean doesn't have a concept of "irreducible fractions" per se,
we just formalize this as saying the numerator and denominator are
relatively prime.
-/
theorem imo1959_p1 : ∀ n : ℕ, Nat.Coprime (21 * n + 4) (14 * n + 3) := sorry


end Imo1959P1

File author(s): Kevin Lacker

This problem has a complete formalized solution.

The solution was imported from mathlib4/Archive/Imo/Imo1959Q1.lean.