Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1979P2

module

public import Mathlib.Tactic

public section


/-!
# International Mathematical Olympiad 1979, Problem 2

A prism with pentagons $A_1A_2A_3A_4A_5$ and $B_1B_2B_3B_4B_5$ as the top and
bottom faces is given. Each side of the two pentagons and each of the 25
segments $A_iB_j$ is colored red or green. Every triangle whose vertices are
vertices of the prism and whose sides have all been colored has two sides of
a different color. Prove that all 10 sides of the top and bottom faces have
the same color.
-/

namespace Imo1979P2

theorem imo1979_p2 (a b : Fin 5 → Bool) (c : Fin 5 → Fin 5 → Bool)
    (ha : ∀ i j : Fin 5, ¬ (a i = c i j ∧ c i j = c (i + 1) j))
    (hb : ∀ i j : Fin 5, ¬ (b j = c i j ∧ c i j = c i (j + 1))) :
    ∃ col : Bool, (∀ i : Fin 5, a i = col) ∧ (∀ i : Fin 5, b i = col) := sorry

end Imo1979P2

File author(s): Kimi K3

This problem has a complete formalized solution.