Oct 6, 2026
Lean formalization in OpenAI math repository (Result 174)
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 strong thin tree conjecture'. We prove that every finite loopless k-edge-connected multigraph on at least two vertices, with k ≥ 1, has a spanning tree meeting each cut in at most C/k times the size of the cut, where C is a universal constant. This resolves the strong thin tree conjecture.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 174). The Lean development was not rebuilt locally.