Oct 6, 2026
Lean formalization in OpenAI math repository (Result 128)
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 'A Polynomial-Time 2-Approximation for Shortest Common Superstring'. We give a deterministic algorithm that, for every finite family of explicitly represented ordinary strings, outputs a common superstring of length at most twice the optimum in time polynomial in the total encoded input size, including symbol labels. The guarantee applies to the algorithm constructed here, not the classical maximum-overlap Greedy procedure.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 128). The Lean development was not rebuilt locally.