Reed's omega, delta, and chi conjecture
For a finite graph , we define to be the maximum degree, to be the size of the largest clique subgraph, and to be the chromatic number. Reed's omega, delta, and chi conjecture states that $$\chi(G) \leq \lceil \frac{1}{2...
Mathematical statement
For a finite graph , we define to be the maximum degree, to be the size of the largest clique subgraph, and to be the chromatic number. Reed's omega, delta, and chi conjecture states that
Statement source: Papers statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
reed_omega_delta_chi_conjecture_for_finite_graphs
theorem reed_omega_delta_chi_conjecture_for_finite_graphs : ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], let χ := G.chromaticNumber let ω := G.cliqueNum let Δ := G.maxDegree 2 * χ ≤ ω + Δ + 2 := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References