Oct 6, 2026
Lean formalization in OpenAI math repository (Result 342)
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 'Taming implies compatibility on four-manifolds'. We prove that every smooth almost complex structure on a closed four-manifold which is tamed by a symplectic form is compatible with a symplectic form. This gives a positive solution to Donaldson's tamed-to-compatible conjecture. We also characterize the compatible cone by strict intersection positivity on the closure of the invariant part of the taming cone.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 342). The Lean development was not rebuilt locally.