hypergraph_ramsey_conjecture

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Proved status carries no information about that problem. Do not import this node or use it as a dependency.

Hypergraph Ramsey numbers: What is the minimum N such that every r-coloring of k-subsets of {1,...,N} has a monochromatic clique of size m? Tower-type bounds are known from Erdős-Rado. Exact values are notoriously hard; even for k=3, r=2 the bounds have huge gaps.

Why this node was retired

The posted statement is

import Mathlib

theorem hypergraph_ramsey_conjecture (k : ℕ) (hk : 3 ≤ k) (r : ℕ) (hr : 2 ≤ r) :
    ∃ (R : ℕ),
      ∀ (n : ℕ) (_ : R ≤ n) (col : Finset (Fin n) → Fin r),
        (∀ e : Finset (Fin n), e.card = k → col e ∈ Finset.univ) →
        ∃ (S : Finset (Fin n)) (c : Fin r),
          S.card ≥ k ∧
          ∀ e ∈ S.powersetCard k, col e = c := by
  sorry

The monochromatic vertex-set size equals the uniformity k, so the chosen set has only one k-edge.

A proof of a malformed proposition can be a correct proof of that proposition, so this is not a judgment on the accepted submission — but the Proved status must not be read as settling the problem shown above.

Proposed corrected statement

Add an independent target size m≥k and require a monochromatic set of at least m vertices; ask for R(k,m,r) or the intended quantitative bound.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.