Oct 6, 2026
Lean formalization in OpenAI math repository (Result 176)
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 'The second Kahn–Kalai conjecture'. We prove the second Kahn–Kalai conjecture. For every finite simple graph H with h ≥ 1 edges and at most n vertices, the threshold for G(n,p) to contain an ordinary copy of H is at most C p_{\mathrm E}(n,H)(1+\log_2 h), where C is universal. Here p_{\mathrm E}(n,H) is the least density at which every subgraph of H has expected copy count at least one half.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 176). The Lean development was not rebuilt locally.