Donaldson's tamed-to-compatible conjecture
From OpenAI Aftermath
Donaldson's tamed-to-compatible conjecture asks whether an almost complex structure on a closed four-manifold that is tamed by a symplectic form, meaning that ω(v, Jv) > 0 for every nonzero tangent vector v, also admits a compatible symplectic form, one that in addition satisfies ω(Ju, Jv) = ω(u, v). Donaldson posed the question in 2006. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), in editions dated 23 September and 6 October 2026, claims an affirmative answer for every closed connected smooth four-manifold, with the almost complex structure kept fixed, and the collection includes a Lean formalization of this statement. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- The question is Section 5.2, Question 2 of Donaldson's 2006 paper, and is distinct from his a priori estimate conjecture for a prescribed-volume equation. Averaging ω with ω(J·, J·) keeps positivity on complex lines but generally loses closedness.
- For integrable J the question belongs to the theory of compact complex surfaces: Buchdahl and Lamari gave classification-free proofs that an even first Betti number implies the existence of a Kähler metric, and Li and Zhang proved that taming and compatible symplectic forms exist together on complex surfaces.
- Through pseudoholomorphic curves, Gromov constructed compatible forms on CP2 for structures tamed by the standard form; Taubes obtained compatibility for a residual set of tamed structures when b2+ = 1; Li and Zhang treated every tamed structure on S2 × S2 and on CP2 # CP2, and further rational manifolds under hypotheses on embedded pseudoholomorphic spheres.
- The condition hJ− = b2+ − 1 on the anti-invariant cohomology appears in Buchdahl-type approaches and in criteria of Wang, Wang and Zhu and of Wang, Zhang, Zheng and Zhu. The current-theoretic approach goes back to Sullivan's cone duality and Harvey and Lawson's characterization of Kähler manifolds through positive currents.
The original result
- Claim. Theorem 1.1 of Taming implies compatibility on four-manifolds states that if a smooth almost complex structure J on a closed connected smooth four-manifold is tamed by a symplectic form, then there is a smooth symplectic form compatible with the same J. No condition is imposed on the cohomology class of the compatible form. A second theorem describes the compatible cone through the taming cone, the anti-invariant cohomology HJ− and the intersection pairing; when hJ− = b2+ − 1 the taming cone equals the compatible cone plus HJ−, so for b2+ = 1 every taming class contains a compatible form.
- Method, as described: if no compatible form exists, a separation argument produces a nonzero positive current annihilating closed invariant forms; an elliptic correction makes it closed up to an anti-invariant part, which regularization shows to be square integrable. Mass and angular estimates for the trace measure lead to the principal step, that the restriction of the current to the points of positive two-dimensional density is closed, and from there to a contradiction with the existence of a taming form.
- Editions. The 23 September edition stated, as a corollary, that the taming cone equals the compatible cone plus HJ− for every tamed J. The 6 October edition restricts this equality to the case hJ− = b2+ − 1 and gives an explicit almost complex structure on the four-torus for which the inclusion is strict.
- Sources (openai/math repository, commit
1581d4c): Taming implies compatibility on four-manifolds (6 October 2026); the earlier edition dated 23 September remains in the repository. - Formalization, as described by the repository. The scope note states that the formalized result establishes the conjecture for every closed connected smooth four-manifold, keeping the almost complex structure fixed, with no integrability assumption or prescribed cohomology class for the compatible form. The Comparator statement is
TamingCompatibility.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 21 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full" and records a Comparator pass for TamingCompatibility. Its note states that differential forms and almost complex structures are hand-built definitions, which it reads as the standard notions. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-09 | Pico (Håkon Åmdal), row 342 in piiiico/openai-math-counterexamples (GitHub; commit 5ff6a94) |
Verification (worked example) | Checks every pointwise claim of the four-torus example added in the 6 October edition: the forms are self-dual as stated, the constructed form is closed and compatible, the two taming forms pair to zero, and the anti-invariant cohomology vanishes. Reports "holds"; the example refutes the cone equality stated in the 23 September edition. | Floating-point checks with exact integer steps; part of a census of counterexample families in the collection. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38019899278 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the TamingCompatibility solution, in 5,143 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal lists TamingCompatibility as the one challenge where con-leche exceeded 25 GB of memory with eight jobs while Lean's official kernel accepts it (8.2 GB); with one job, con-leche accepts it (11.4 GB, 390 s). |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap and no minor note. The reviewer states that it read every section and checked each step of the main proof line by line. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
