Skip to content

Erdős problem 775

Is there a 33-uniform hypergraph on nn vertices which contains at least n−O(1)n-O(1) different sizes of cliques (maximal complete subgraphs)?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/775.lean

Formal Conjectures

FormalConjectures/ErdosProblems/775.leanErdos775.erdos_7751 lineExact file
False ↔ ∃ C, ∃ᶠ (n : ℕ) in Filter.atTop, ∃ H, n - C ≤ H.cliqueSizes.ncard
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:775
  • PLBY Lean proofsErdosProblems.Erdos775

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page