OAI.SharpLogRamsey.main

Proved

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

The theorem states that for every natural number s ≥ 6, two properties hold for the Ramsey numbers R(s,t), where R(s,t) is defined as the least N such that every simple graph on N labeled vertices contains either a clique of size s or an independent set of size t. First, there is a constant C > 0, chosen independently of ε, such that for every ε > 0 there is a threshold t₀ with the following holding for all t ≥ t₀: t^(s−1) / (log t)^((s−2)+ε) ≤ R(s,t) and R(s,t) ≤ C · t^(s−1) / (log t)^(s−2). Second, the quantity ((s−1)·log t − log R(s,t)) / log log t tends to s−2 as t tends to infinity through the natural numbers.

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/SharpLogRamsey.lean; bytes 1097..1179
-- 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_SharpLogRamsey

namespace OAI

namespace SharpLogRamsey

Formal statement

theorem main (s : ℕ) (hs : 6 ≤ s) : MainBounds s ∧ MainLimit s := by
  sorry

end SharpLogRamsey
end OAI

Source

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

Human review

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

View graph