View source for Donaldson's tamed-to-compatible conjecture

'''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'') &gt; 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 ([https://github.com/openai/math 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 '''CP'''<sup>2</sup> for structures tamed by the standard form; Taubes obtained compatibility for a residual set of tamed structures when ''b''<sub>2</sub><sup>+</sup> = 1; Li and Zhang treated every tamed structure on ''S''<sup>2</sup> × ''S''<sup>2</sup> and on '''CP'''<sup>2</sup> # <span style="text-decoration:overline">'''CP'''</span><sup>2</sup>, and further rational manifolds under hypotheses on embedded pseudoholomorphic spheres.
** The condition ''h''<sub>''J''</sub><sup>&minus;</sup> = ''b''<sub>2</sub><sup>+</sup> &minus; 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 ''H''<sub>''J''</sub><sup>&minus;</sup> and the intersection pairing; when ''h''<sub>''J''</sub><sup>&minus;</sup> = ''b''<sub>2</sub><sup>+</sup> &minus; 1 the taming cone equals the compatible cone plus ''H''<sub>''J''</sub><sup>&minus;</sup>, so for ''b''<sub>2</sub><sup>+</sup> = 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 ''H''<sub>''J''</sub><sup>&minus;</sup> for every tamed ''J''. The 6 October edition restricts this equality to the case ''h''<sub>''J''</sub><sup>&minus;</sup> = ''b''<sub>2</sub><sup>+</sup> &minus; 1 and gives an explicit almost complex structure on the four-torus for which the inclusion is strict.
* '''Sources''' (openai/math repository, commit <code>1581d4c</code>): [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Taming-implies-compatibility-on-four-manifolds-October-6-2026 ''Taming implies compatibility on four-manifolds''] (6 October 2026); the earlier edition [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Taming-implies-compatibility-on-four-manifolds-September-23-2026 dated 23 September] remains in the repository.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/342.md 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 <code>TamingCompatibility.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 21 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates this family "full" and records a Comparator pass for <code>TamingCompatibility</code>. 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 [https://github.com/piiiico/openai-math-counterexamples/tree/5ff6a94fe81c4a9d620689a078b0f80060c17ab8/rows/342 piiiico/openai-math-counterexamples] (GitHub; commit <code>5ff6a94</code>) || 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 [https://github.com/carlostoledo1891/cert-machine/blob/32739df1a7e9b09f6b56216444fa32927ffdeaad/corpus/openai-math/kernel-runs/38019899278/TamingCompatibility.json 38019899278] || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>TamingCompatibility</code> 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal lists <code>TamingCompatibility</code> 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, [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_426.json referee review] in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 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.

[[Category:OpenAI results]]