Oct 6, 2026
Lean formalization in OpenAI math repository (Result 175)
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 'Talagrand's discrete-convexity conjecture'. We prove Talagrand's discrete-convexity conjecture. There is a universal integer k such that, whenever an arbitrary family has Bernoulli product measure at least 1-1/k, the sets not contained in a union of k members admit a cover of total cost at most 1/2 at the same density.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 175). The Lean development was not rebuilt locally.