Donaldson's tamed-to-compatible conjecture for almost complex four-manifolds
Let be a closed smooth four-manifold with a smooth almost complex structure . A symplectic form tames if for all nonzero tangent vectors , and is compatible with if moreover . Donaldson asked whether a tamed by some symplectic form must also admit a compatible symplectic form. Known cases: integrable (complex surfaces, via Buchdahl, Lamari and Li-Zhang), (Gromov), generic tamed when (Taubes), and some rational surfaces (Li-Zhang), and conditional results under . If an almost complex structure on a closed four-manifold is tamed by a symplectic form, is it compatible with some symplectic form?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Symplectic geometry of four-manifolds; almost complex structures
- Posed by
- S. K. Donaldson, Two-forms on four-manifolds and elliptic equations, in Inspired by S. S. Chern (2006), Section 5.2, Question 2
- Year posed
- 2006
- Years open
- 20y
- Solved
- 2026-09-23
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 45 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: if a smooth almost complex structure on a closed connected smooth four-manifold is tamed by a symplectic form, there is a smooth symplectic form compatible with the same . Corollary (with Li-Zhang): the taming cone equals the compatible cone plus the anti-invariant cohomology , and when every taming class contains a compatible representative. Not shown: that an arbitrary taming class contains a compatible form when , anything in dimensions above four, or Donaldson's separate a priori estimate conjecture for the prescribed-volume equation.
What the AI did
Produced by an unreleased internal OpenAI model as part of an OpenAI evaluation on open research problems, published in the openai/math release (pinned commit adc7f12). The release README says the vast majority of results used one fixed procedure, averaging about three hours of ChatGPT Pro thinking compute per result; this result is not among the README's stated exceptions (the Riemann zeta zero-free region work and the Hodge conjecture for CM abelian varieties). The manuscript is authored as OpenAI with no human author named. The main theorem has a Lean formalization in the release (Comparator challenge TamingCompatibility).
Verification
No independent mathematician has checked this yet. Checked here: abstract, introduction and Theorem 1.1 of the TeX source, read against Donaldson's question as cited. Lean-checked on the release's Comparator challenge TamingCompatibility (declaration OAI.TamingCompatibility.taming_implies_compatibility, listed in lean/formalization.yaml). Its statement was read here: for a compact connected Hausdorff second-countable smooth manifold modelled on R^4 and a smooth almost complex structure with , if some symplectic two-form tames then some symplectic two-form tames and is -invariant. Two-forms, smoothness and closedness are encoded by hand through pullbacks along smooth chart maps rather than Mathlib's differential forms; that encoding was read but not audited in depth. It states the headline claim, with the same and no cohomology class prescribed. Not rebuilt here. The manuscript notes that Lin and Zhou questioned estimates in an earlier conditional result (Tan-Wang-Zhou-Zhu 2022); that concerns prior work, not this proof.