Oct 6, 2026
Lean formalization in OpenAI math repository (Result 117)
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 'Near-square-root logarithmic integrality gaps for uniform sparsest cut'. We construct uniform sparsest-cut instances whose Goemans–Linial semidefinite integrality gap is at least c\sqrt{\log n}/(\log\log n)^3 along a sequence n\to\infty. The demand is one between every pair of distinct vertices, and the capacities are nonnegative real numbers. This matches the Arora–Rao–Vazirani upper bound up to a power of \log\log n.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 117). The Lean development was not rebuilt locally.