Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1991P4

module

public import Mathlib.Tactic
public import Mathlib.Combinatorics.SimpleGraph.Trails
public import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
public import Mathlib.Algebra.GCDMonoid.Finset

public section


/-!
# International Mathematical Olympiad 1991, Problem 4

Suppose G is a connected graph with k edges. Prove that it is possible to
label the edges 1, 2, ... , k in such a way that at each vertex which belongs
to two or more edges, the greatest common divisor of the integers labeling
those edges is equal to 1.
-/

namespace Imo1991P4

open SimpleGraph Finset

variable {V : Type*} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj]

theorem imo1991_p4 {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
    [DecidableRel G.Adj] (hG : G.Connected) :
    ∃ Φ : G.edgeSet → ℕ,
      (∀ e : G.edgeSet, 1 ≤ Φ e ∧ Φ e ≤ Fintype.card G.edgeSet) ∧
      (Function.Injective Φ) ∧
      (∀ v : V, 2 ≤ G.degree v →
        ((G.incidenceFinset v).attach.gcd fun ⟨x, h⟩ =>
          Φ ⟨x, mem_edgeFinset.mp <| incidenceFinset_subset G v h⟩) = 1) := sorry

end Imo1991P4

File author(s): Kimi K3

This problem has a complete formalized solution.