# Donaldson's tamed-to-compatible conjecture

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

- [Taming implies compatibility on four-manifolds](../../preprints/Taming-implies-compatibility-on-four-manifolds-September-23-2026/paper.pdf)

## 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](../ComparatorChallenges/TamingCompatibility.lean) |