AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Integral and fractional expectation thresholds are equivalent

Can the mathematical statement in Integral and fractional expectation thresholds are equivalent be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
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 'Integral and fractional expectation thresholds are equivalent'. We prove Talagrand's conjecture that integral and fractional expectation thresholds are within a universal constant factor, with the same covering budget.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 175). The Lean development was not rebuilt locally.