Oct 6, 2026
Lean formalization in OpenAI math repository (Result 162)
Model / AI: OpenAI (unreleased)
machine-checked (counterexample)self-reported (counterexample)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A counterexample to Ryser's covering conjecture'. For every sufficiently large prime s\equiv2\pmod3 and every sufficiently large odd integer n, with the threshold depending on s, we construct an intersecting (s^n+1)-partite (s^n+1)-uniform hypergraph with covering number s^n+1. This disproves Ryser's covering conjecture in its intersecting case.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 162). The Lean development was not rebuilt locally.