Oct 6, 2026
Lean formalization in OpenAI math repository (Result 184)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A logarithmic independence bound for clique-free graphs'. For every fixed integer r ≥ 4, every Kr-free graph on n vertices with average degree d ≥ 2 has an independent set of size at least c_r n\log d/d, where c_r\gt 0 depends only on r. This proves the fixed-clique-size independence conjecture of Ajtai, Erdős, Komlós and Szemerédi.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 184). The Lean development was not rebuilt locally.