Tamed means compatible?
An AI preprint claims that taming always upgrades to compatibility on closed four-manifolds
Covers result 342 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
3:51. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
An almost complex structure turns each tangent space of a four-manifold into a copy of complex two-space. A symplectic form tames it if it is positive on every complex line, and is compatible if, in addition, the structure leaves it unchanged. Compatible is much stricter: at a single point, our computer finds that about 9 percent of random two-forms tame the standard structure, while compatible ones form a thin slice. Averaging a closed taming form pointwise makes it compatible but, as our computer shows, can destroy closedness.
In 2006 Donaldson asked: if an almost complex structure on a compact four-manifold is tamed by a symplectic form, is there a symplectic form compatible with it? For manifolds with b⁺ = 1, Tosatti, Weinkove and Yau stated it as a conjecture, and in 2009 Taubes proved it for generic structures. Complex surfaces were settled, and in 2022 Tan, Wang, Zhou and Zhu published a claimed proof of a further case, which includes every structure when b⁺ = 1; later work questioned some steps. The general case had no claimed proof.
Result 342 is one OpenAI paper. The first version, 18 pages dated September 23, went public October 6; a 23-page revision dated October 6 was added the next day. It claims the answer is yes on every closed, connected four-manifold: if a smooth almost complex structure is tamed by a symplectic form, some symplectic form is compatible with that same structure. The form’s cohomology class may have to change.
What it doesn’t claim
Not claimed: that every taming class contains a compatible form. The first version did state a general formula linking taming and compatible classes, citing a 2009 paper; the revision replaces it with a corrected statement and an explicit four-torus example where the old formula fails. Our computer checks that example: two taming classes whose product is zero, so neither contains a compatible form. The proof of the main theorem is unchanged.
Where it stands
- Posted as a preprint
- OpenAI, dated September 23, 2026; revised October 7 (class formula corrected; main proof unchanged)
- Peer reviewed
- Not yet
- Formalized in Lean
- The main theorem; not the class results (docs)
Last checked October 19, 2026. The paper is unrefereed. Its main theorem is formalized in Lean, in about 580 files and 83,000 lines, not run by us; two outside projects re-ran the check, one also with a second kernel, and it passed. The class statement and the four-torus example are not formalized. We found no specialist comment and no reported error in the main theorem. OSVerify has not reviewed it.
How the proof goes
- Suppose no compatible form exists. The proof argues by contradiction, without holomorphic curves or Seiberg–Witten theory. If no compatible form existed, a separation argument would produce a positive current, a weighted cloud of complex lines, which an elliptic correction completes to a closed current. The paper shows this cloud has at most quadratic mass growth, and heat-kernel smoothing shows that nearby complex lines are nearly parallel.
- A contradiction from positivity. The key step: the part of the cloud with positive density is itself closed. A final pairing forces the correction to vanish, leaving a positive current that gives zero on every closed form, yet the taming form must pair with it positively. That is the contradiction. Positivity drives the class results too: at a single point, our computer finds that a compatible form and a taming form always have positive wedge product, in 90,000 random pairs, while two taming forms need not.
The numbers in the video
- Ours: at a point, about 9.2% of random 2-forms tame the standard almost complex structure; compatible ones form a thin slice.
- Ours: a compatible form and a taming form always have positive wedge product (90,000 of 90,000 random pairs), while two taming forms need not (8,074 of 90,000 fail).
- Ours: the paper’s four-torus example checked on a grid: two taming classes with product 0, so neither has a compatible representative.
- Lean: 582 files and 83,060 lines in the import closure (counted by us; not run by us).
Read the source
- Taming implies compatibility on four-manifolds (PDF), 23 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 342.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
An almost complex structure turns each tangent space of a four-manifold into a copy of complex two-space. A symplectic form tames it if it is positive on every complex line, and is compatible if, in addition, the structure leaves it unchanged. Compatible is much stricter: at a single point, our computer finds that about 9 percent of random two-forms tame the standard structure, while compatible ones form a thin slice. Averaging a closed taming form pointwise makes it compatible but, as our computer shows, can destroy closedness. In 2006 Donaldson asked: if an almost complex structure on a compact four-manifold is tamed by a symplectic form, is there a symplectic form compatible with it? For manifolds with b⁺ = 1, Tosatti, Weinkove and Yau stated it as a conjecture, and in 2009 Taubes proved it for generic structures. Complex surfaces were settled, and in 2022 Tan, Wang, Zhou and Zhu published a claimed proof of a further case, which includes every structure when b⁺ = 1; later work questioned some steps. The general case had no claimed proof.
1:13The claim
Result 342 is one OpenAI paper. The first version, 18 pages dated September 23, went public October 6; a 23-page revision dated October 6 was added the next day. It claims the answer is yes on every closed, connected four-manifold: if a smooth almost complex structure is tamed by a symplectic form, some symplectic form is compatible with that same structure. The form’s cohomology class may have to change. Not claimed: that every taming class contains a compatible form. The first version did state a general formula linking taming and compatible classes, citing a 2009 paper; the revision replaces it with a corrected statement and an explicit four-torus example where the old formula fails. Our computer checks that example: two taming classes whose product is zero, so neither contains a compatible form. The proof of the main theorem is unchanged.
2:13How the proof goes
The proof argues by contradiction, without holomorphic curves or Seiberg–Witten theory. If no compatible form existed, a separation argument would produce a positive current, a weighted cloud of complex lines, which an elliptic correction completes to a closed current. The paper shows this cloud has at most quadratic mass growth, and heat-kernel smoothing shows that nearby complex lines are nearly parallel. The key step: the part of the cloud with positive density is itself closed. A final pairing forces the correction to vanish, leaving a positive current that gives zero on every closed form, yet the taming form must pair with it positively. That is the contradiction. Positivity drives the class results too: at a single point, our computer finds that a compatible form and a taming form always have positive wedge product, in 90,000 random pairs, while two taming forms need not.
3:12Where it stands
The paper is unrefereed. Its main theorem is formalized in Lean, in about 580 files and 83,000 lines, not run by us; two outside projects re-ran the check, one also with a second kernel, and it passed. The class statement and the four-torus example are not formalized. We found no specialist comment and no reported error in the main theorem. If it holds, Donaldson’s question has a yes answer on every closed four-manifold: taming always upgrades to compatibility, though not always in the same cohomology class.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.