E579: “Dense octahedron-free graphs have linear independence number.”

Open

Statement	User	Model	Harness	Time
2)V2At the extremal half-density boundary, the requested linear independent-set conclusion holds: no nonempty fin…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1For every positive density δ, every sufficiently large octahedron-free graph on n vertices with at least δn²…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 At the extremal half-density boundary, the requested linear independent-set conclusion holds: no nonempty finite simple graph has at least n²/2 edges.

kernel-checked, filed Tue Aug 25 2026 05:34:56 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. The fixed density coefficient δ=1/2; all finite simple graphs, with the root octahedron-free hypothesis retained.

1) V1 For every positive density δ, every sufficiently large octahedron-free graph on n vertices with at least δn² edges has an independent set of size at least cδ n for some positive cδ.

open, filed Tue Aug 25 2026 05:29:14 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Root canonical statement. The outer `answer(sorry) ↔` metadata wrapper from Formal Conjectures is removed while preserving its concrete right-hand proposition. The positive constant is selected before the eventual quantifier, so it is uniform in n and G.

Scope. Finite simple graphs on Fin n; the forbidden octahedron is K₂,₂,₂; c may depend on δ but not on n or the graph.

E579:Erdős Problem #579 “Dense octahedron-free graphs have linear independence number.”

E579: “Dense octahedron-free graphs have linear independence number.”