Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1975P5

import Mathlib

/-!
# International Mathematical Olympiad 1975, Problem 5

Determine, with proof, whether or not one can find $1975$ points on the circumference of a circle
with unit radius such that the distance between any two of them is a rational number.
-/

namespace Imo1975P5

/- determine -/ abbrev constructible : Bool := sorry

theorem imo1975_p5 : constructible ↔
    ∃ p : Finset Circle, p.card = 1975 ∧ (SetLike.coe p).Pairwise (fun a b => ¬ Irrational (dist a b)) := sorry

end Imo1975P5

File author(s): Constantin Seebach

This problem has a complete formalized solution.