Erdős problem 1080 · problems.science

Let $G$ be a bipartite graph on $n$ vertices such that one part has $\lfloor n^{2/3}\rfloor$ vertices. Is there a constant $c>0$ such that if $G$ has at least $cn$ edges then $G$ must contain a $C_6$ ?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/1080.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1080.leanErdos1080.erdos_10806 linesExact file

1False ↔2  ∃ c > 0,3    ∀ (V : Type) [inst : Fintype V] [Nonempty V] (G : SimpleGraph V) (X Y : Set V),4      Erdos1080.IsBipartition G X Y →5        X.ncard = ⌊↑(Fintype.card V) ^ (2 / 3)⌋₊ →6          ↑G.edgeSet.ncard ≥ c * ↑(Fintype.card V) → ∃ v walk, walk.IsCycle ∧ walk.length = 6

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:1080
PLBY Lean proofsErdosProblems.Erdos1080

Reported activity

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

Formalization
Erdős AI contributions wiki · 28 Dec, 2025
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