Donaldson's tamed-to-compatible conjecture

1 paperLean

Proves Donaldson's tamed-to-compatible conjecture: every smooth almost complex structure on a closed four-manifold that is tamed by a symplectic form admits a compatible symplectic form. The almost complex structure stays fixed; the form's cohomology class may change.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 1

Taming implies compatibility on four-manifolds

OpenAI · October 6, 2026

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.

This version characterizes the compatible cone by intersection positivity, restricts the cone-sum equality to \(h_J^-=b_2^+-1\), and adds a four-torus example of strict inclusion; see the previous version.

Read PDF Download Source

Cite

@misc{OAI:Taming-implies-compatibility-on-four-manifolds-October-6-2026,
  author = {{OpenAI}},
  title = {{Taming implies compatibility on four-manifolds}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Taming-implies-compatibility-on-four-manifolds-October-6-2026/paper.pdf}{OAI:Taming-implies-compatibility-on-four-manifolds-October-6-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Taming implies compatibility on four-manifolds

Scope

Donaldson's tamed-to-compatible conjecture asks whether an almost-complex structure tamed by a symplectic form also admits a compatible symplectic form. The formalized result establishes this for every closed connected smooth four-manifold, keeping the almost-complex structure fixed. No integrability assumption or prescribed cohomology class for the compatible form is required.

Comparator links

Result	Comparator statement
Taming implies compatibility	TamingCompatibility.lean

Scope note on GitHub →