Taming implies compatibility on four-manifolds

Follow-up works

• OpenAI, Deforming hypersymplectic four-manifolds to hyperkähler triples (OpenAI Math Release preprint, 2026-10-07). This companion manuscript explicitly reuses the taming paper’s current estimates and density-splitting argument, adding prescribed-class arguments under closed definite-pair and $b^+=3$ hypotheses for its claimed hypersymplectic deformation theorem. [AI-generated per source]

Formalization

• OpenAI math release, Lean scope note for family 342 (Donaldson's tamed-to-compatible conjecture) (lean/docs/342.md, 2026). The release's scope note says the formalized result covers every closed connected smooth four-manifold with $J$ fixed, with no integrability assumption and no prescribed cohomology class; it links the September 23 edition of the paper and its comparator statement. [cites earlier version]
• OpenAI, TamingCompatibility.lean (openai/math, lean/ComparatorChallenges, 2026). A 68-line Lean 4/Mathlib Comparator statement of Theorem 1.1 (taming_implies_compatibility) for compact connected manifolds modelled on $\mathbb R^4$, with its own definitions of two-forms, closedness via pullbacks to charts, taming and compatibility; the proof in this statement file is sorry.

Possibly relevant literature (found by the agent, not checked)

• Tedi Draghici, Tian-Jun Li and Weiyi Zhang, Symplectic forms and cohomology decomposition of almost complex 4-manifolds (arXiv:0812.3680; International Mathematics Research Notices 2010, no. 1, 1–17). Its decomposition of second cohomology into $J$-invariant and anti-invariant subspaces and dimension estimates for tamed structures provide background for the manuscript’s cone theorem and the condition $h_J^-=b_2^+-1$.
• Qiang Tan and Haifeng Xu, A Note on Donaldson's "Tamed to Compatible" Question (Communications in Mathematical Research 30(2), 2014). Gives another proof of the Draghici–Zhang reformulation of Donaldson's question (compatible form exists iff tamed forms with arbitrary anti-invariant parts exist), which is related to the paper's cone decomposition $\mathcal K_J^t=\mathcal C+H_J^-$.
• Pranav Chakravarthy, Jordan Payette and Martin Pinsonnault, J-tamed inflation via tame to compatible deformations (arXiv:2403.19110, 2024; v2 2025). Proves a "preparation lemma" making a taming form compatible along a $J$-holomorphic submanifold within its cohomology class, which the authors call an infinitesimal version of the conjecture; it bears on the paper's remark that Theorem 1.1 does not fix the cohomology class.
• Valentino Tosatti, Ben Weinkove and Shing-Tung Yau, Taming symplectic forms and the Calabi-Yau equation (Proc. London Math. Soc. 97, 2008). Studies Donaldson's a priori estimate conjecture for the symplectic Calabi–Yau equation with a taming form, the related problem that the paper's introduction says is distinct from the existence question it answers.
• Spencer Cattalani, Positivity of Intersections and Tameness of Almost Complex 4-manifolds (arXiv:2401.17381, Selecta Math. 2026). Constructs taming forms from families of pseudoholomorphic curves along the lines Gromov proposed, which is related to the curve-based approach (Gromov, Taubes, Li–Zhang) that the paper contrasts with its current-based argument.

News and blogs

• Gautam Parab, OpenAI’s First Math Errata: Three Papers Outside the Lean Catalogue, and One Corollary the Lean Never Covered (blog, 2026-10-15). The section “The one with Lean” compares the September 23 and October 6 cone statements and explains that the corrected corollary lies outside the release’s stated formalization scope.
• MINT Research, Yesterday in AI · 8 October 2026 (newsletter, 2026-10-08). Its report on the release’s corrections describes this paper’s narrowed cone equality and four-torus example, distinguishing them from the main existence theorem covered by the Lean scope note. [AI-generated per source]
• MarsBit / Machine Heart (republished by KuCoin News), OpenAI Withdraws Three AI Mathematics Papers Due to Sign Error in Key Proof (KuCoin News flash, 2026-10-08). The article mentions family 342 (calling it the "tame pushout compatibility" conjecture) as revised, not withdrawn: the main conclusion stands, and an overstated auxiliary claim was narrowed and given a counterexample.