Erdős problem 1008 · problems.science

Does every graph with $m$ edges contain a subgraph with $\gg m^{2/3}$ edges which contains no $C_4$ ?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/1008.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1008.leanErdos1008.erdos_10084 linesExact file

1True ↔2  ∃ c > 0,3    ∀ (V : Type) [Fintype V] (G : SimpleGraph V),4      ∃ H ≤ G, (SimpleGraph.cycleGraph 4).Free H ∧ c * ↑G.edgeSet.ncard ^ (2 / 3) ≤ ↑H.edgeSet.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:1008
PLBY Lean proofsErdosProblems.Erdos1008

Reported activity

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

Formalization
Erdős AI contributions wiki · 17 Jan, 2026
Machine
Aristotle
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science