OAI.CliqueFreeLog.logarithmic_independence_bound

Open

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that, for every natural number r ≥ 4, there is a real constant c > 0 such that the following holds for every finite simple graph G on a vertex type V (a Fintype). Here the average degree d(G) is defined as 2|E(G)|/|V|, twice the number of edges divided by the number of vertices (as a real number). If G contains no clique of size r (it is r-clique-free) and d(G) ≥ 2, then the independence number α(G), the maximum size of an independent set, satisfies α(G) ≥ c · |V| · log(d(G)) / d(G), where log is the natural logarithm of real numbers. The constant c may depend on r but not on G. The statement is admitted without proof in the source.

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/CliqueFreeLog.lean; bytes 220..548
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_CliqueFreeLog

namespace OAI

namespace CliqueFreeLog

Formal statement

theorem logarithmic_independence_bound (r : ℕ) (hr : 4 ≤ r) :
    ∃ c : ℝ, 0 < c ∧
      ∀ {V : Type} [Fintype V] (G : SimpleGraph V),
        G.CliqueFree r → 2 ≤ averageDegree G →
        c * (Fintype.card V : ℝ) * Real.log (averageDegree G) / averageDegree G ≤
          (G.indepNum : ℝ) := by
  sorry

end CliqueFreeLog
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/CliqueFreeLog.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by marwahaha · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph