Oct 6, 2026
Lean formalization in OpenAI math repository (Result 143)
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 'Two limit cycles for quintic Liénard systems'. Every classical Liénard system \dot x=y-F(x), \dot y=-x, with F an arbitrary real polynomial of degree at most five, has at most two geometrically distinct isolated periodic orbits, and the bound is attained. This proves the degree-five case of the Lins Neto–de Melo–Pugh conjecture.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 143). The Lean development was not rebuilt locally.