Search

Donaldson's tamed-to-compatible conjecture

Proves Donaldson's tamed-to-compatible conjecture for tamed almost-complex structures on closed four-manifolds.

1 paper October 6, 2026 Explained by AI

An almost-complex structure rotates each direction in a four-dimensional space by a right angle. A symplectic form is a closed rule for measuring signed area. Taming asks that the form be positive on each direction and its rotation, and compatibility also asks that the rotation not change the form. Donaldson asked in 2006 whether taming always gives a compatible form on closed four-manifolds. The paper proves yes, and Lean, a computer proof checker, has a formal statement of this result.

First step
2006
Simon Donaldson, Question 2 in his study of two-forms on four-manifolds
Significance
Major
It settles, with a Lean statement, a well-known conjecture of Donaldson in four-dimensional symplectic geometry.
Trust
Formal proof listed
Field
Differential geometry
1 paper

The explanation

Work in four-dimensional space with coordinates x1 to x4. Let J rotate directions by a right angle: J sends (v1, v2, v3, v4) to (−v2, v1, −v4, v3). Take the area form ω = dx1 dx2 + dx3 dx4. For any direction v, ω(v, Jv) equals v1² + v2² + v3² + v4², which is positive. Now add c dx1 dx3. This extra term gives −v1v4 + v2v3 on the pair v, Jv. For v = (1, 0, 0, 1), the total is 2 − c. With c = 1 it is 1, still positive. With c = 3 it is −1, so positivity fails.

A two-form ω tames J if ω(v, Jv) is positive for every nonzero v. It is compatible if also ω(Ju, Jv) = ω(u, v). With c = 1 the form tames J but is not compatible. Averaging it with its rotated copy gives dx1 dx2 + dx3 dx4 + (c/2)(dx1 dx3 + dx2 dx4), which is compatible. A symplectic form is a closed nondegenerate two-form, and closed means its derivative is zero. Here the coefficients are constant, so the average stays closed. On a curved four-manifold, where J changes from point to point, this averaging keeps positivity but usually loses closedness. That is the obstacle.

Donaldson asked in 2006 whether a taming symplectic form on a closed four-manifold implies a compatible one exists. Li and Zhang proved this for complex surfaces, where J comes from complex coordinates. Taubes proved it for most tamed J when one topological number, b₂⁺, equals 1. Li and Zhang extended this to some rational four-manifolds.

The paper proves the general case. The compatible form works for the given J, but its cohomology class, a kind of fixed label, is not prescribed. The proof argues by contradiction. If no compatible form existed, a separation argument would give a nonzero positive current, a kind of generalized surface, that kills all closed invariant forms. The main step shows that the part of this current with positive two-dimensional density is closed. Then the correction term must vanish, and the current cannot coexist with a closed taming form. The paper also describes exactly which classes hold compatible forms. When b₂⁺ = 1, every taming class has a compatible form. A four-torus example shows this can fail in general.

How sure is this? Lean, a computer proof checker, has a formal statement of the main result for every closed connected four-manifold, with J kept fixed. So the paper proves this result, as far as the Lean statement matches the paper. The cone description and the four-torus example are not listed in the Lean scope. No specialist review is published.

What it doesn't show. This does not say that every taming cohomology class contains a compatible form; it can fail when the anti-invariant dimension is small.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

Major, with a Lean statement of the main theorem. It does not put a compatible form in every taming class. No specialist review is published.

Words used

Almost-complex structure
A rule J that rotates each tangent direction by a right angle, so applying it twice reverses the direction.
Two-form
A rule that assigns a signed area to each pair of directions.
Symplectic form
A closed two-form that is nondegenerate, so no direction pairs to zero with every other.
Tame
A two-form tames J if it is positive on every nonzero direction paired with its rotation by J.
Compatible
Taming, and also unchanged when both directions are rotated by J.
Cohomology class
A label for a closed form that stays fixed under certain allowed changes.
Positive current
A generalized surface, possibly spread out, that pairs positively with taming forms.
b₂⁺
The number of independent positive directions in how surfaces in the four-manifold intersect.

The original paper

Lean notes

All quoted lines (13)
  1. A real two-form ω\omega tames JJ if ω(v,Jv)>0\omega(v,Jv)>0 for every nonzero tangent vector vv.
    Taming implies compatibility on four-manifolds Back to text
  2. It is compatible with JJ if, in addition, ω(Ju,Jv)=ω(u,v)\omega(Ju,Jv)=\omega(u,v).
    Taming implies compatibility on four-manifolds Back to text
  3. The elementary projection ω↦12(ω+ω(J ⋅,J ⋅))\omega\mapsto \frac12(\omega+\omega(J\,\cdot,J\,\cdot)) shows the obstacle: it preserves positivity on complex lines but generally loses closedness.
    Taming implies compatibility on four-manifolds Back to text
  4. Donaldson asked whether the existence of a taming symplectic form on a closed four-manifold implies the existence of a compatible one.
    Taming implies compatibility on four-manifolds Back to text
  5. Li and Zhang proved the equivalence between the existence of taming and compatible symplectic forms on complex surfaces.
    Taming implies compatibility on four-manifolds Back to text
  6. Taubes developed integration over curve moduli spaces to obtain compatibility for a residual subset of the smooth almost complex structures tamed by a fixed symplectic form when b2+=1b_2^+=1.
    Taming implies compatibility on four-manifolds Back to text
  7. Li and Zhang extended this approach to every tamed structure on S2×S2S^2\times S^2 and CP2#CP‾2\mathbb{CP}^2\#\overline{\mathbb{CP}}{}^2, and to further rational manifolds under hypotheses on embedded pseudoholomorphic spheres.
    Taming implies compatibility on four-manifolds Back to text
  8. Suppose that a smooth almost complex structure JJ on a closed connected smooth real four-manifold XX is tamed by a symplectic form. Then there is a smooth symplectic form compatible with JJ.
    Taming implies compatibility on four-manifolds Back to text
  9. The conclusion imposes no condition on the cohomology class of the compatible form.
    Taming implies compatibility on four-manifolds Back to text
  10. If no compatible form exists, separation produces a nonzero positive current PP that annihilates closed invariant forms.
    Taming implies compatibility on four-manifolds Back to text
  11. The principal step, Theorem …, proves that the restriction PE=\indEPP_E=\ind_E P is closed.
    Taming implies compatibility on four-manifolds Back to text
  12. In particular, if b2+(X)=1b_2^+(X)=1, then KJt=KJc\mathcal K_J^t=\mathcal K_J^c: every taming class has a smooth compatible symplectic representative.
    Taming implies compatibility on four-manifolds Back to text
  13. The inclusion KJc+HJ−⊆KJt\mathcal K_J^c+H_J^-\subseteq\mathcal K_J^t can be strict when hJ−<b2+−1h_J^-<b_2^+-1, even if HJ−=0H_J^-=0; Example … gives an explicit four-torus.
    Taming implies compatibility on four-manifolds Back to text

Other sources

  1. openai/math, Lean scope note for family 342 The formalized result establishes this for every closed connected smooth four-manifold, keeping the almost-complex structure fixed.
  2. openai/math release notes (2026): model provenance and review status manuscripts and supporting proof artifacts produced by an internal OpenAI model

Browse Differential geometry Named conjecturesOpen since the 2000sLean-checked results