Erdős problem 1034 · problems.science

Let $G$ be a graph on $n$ vertices with $>n^2/4$ many edges. Must there be a triangle $T$ in $G$ and vertices $y_1,\ldots,y_t$ , where $t>(\frac{1}{2}-o(1))n$ , such that every $y_i$ is joined to at least two vertices of $T$ ?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/1034.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1034.leanErdos1034.erdos_10347 linesExact file

1False ↔2  ∀ (ε : ℝ),3    0 < ε →4      ∀ᶠ (n : ℕ) in Filter.atTop,5        ∀ (G : SimpleGraph (Fin n)),6          ↑n ^ 2 / 4 < ↑G.edgeSet.ncard →7            ∃ T, G.IsNClique 3 T ∧ ∃ Y, Erdos1034.JoinedToTwo G T Y ∧ (1 / 2 - ε) * ↑n < ↑Y.card

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:1034
PLBY Lean proofsErdosProblems.Erdos1034

Reported activity

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

Formalization
Erdős AI contributions wiki · 4 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