Formal target: Corpus.Erdos617.erdos_617

Let $r\geq 3$.

Exact formal statement

∀ (r : Nat),
  GE.ge.{0} r 3 →
    ∀ {V : Type} [inst : Fintype.{0} V] [DecidableEq.{1} V],
      Eq.{1} (Fintype.card.{0} V) (HAdd.hAdd.{0, 0, 0} (HPow.hPow.{0, 0, 0} r 2) 1) →
        ∀ (coloring : Sym2.{0} V → Fin r),
          Exists.{1} fun S =>
            Exists.{1} fun k =>
              And (Eq.{1} (Finset.card.{0} S) (HAdd.hAdd.{0, 0, 0} r 1))
                (∀ (u : V),
                  Membership.mem.{0, 0} S u →
                    ∀ (v : V), Membership.mem.{0, 0} S v → Ne.{1} u v → Ne.{1} (coloring (Sym2.mk.{0} u v)) k)

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record