A mathematical preprint on arXiv claims a proof of Étienne Ghys’s conjecture for codimension-one holomorphic Anosov diffeomorphisms, and says an internal version of Shanghai AI Lab’s Intern-S2 science model helped develop the ideas. A Peking University team has formalised the core theorems in the Lean proof assistant, with code on GitHub.
The paper is a preprint. It has not been peer-reviewed. TSN has not verified the mathematics.
What the paper claims
In arXiv:2609.37695v3 (last revised 13 October 2026), sole author Jiesong Zhang writes in the abstract:
We prove that every codimension-one holomorphic Anosov diffeomorphism of a compact connected complex manifold is biholomorphically conjugate to a hyperbolic automorphism of a complex torus. This verifies a conjecture of Ghys in the codimension-one case and, in particular, in complex dimension three.
In plain English: for a certain class of chaotic, structure-preserving maps on complex spaces (Anosov diffeomorphisms that are holomorphic and of codimension one), the paper says each such map is equivalent, via a holomorphic change of coordinates, to a standard hyperbolic map on a complex torus. Ghys proposed related conjectures in 1995; this preprint addresses the codimension-one case.
How Intern-S2 is credited
Zhang’s “Declaration of AI Use” in the paper says he “used an internal version of Intern-S2 to assist in developing the mathematical ideas and arguments presented in this paper through multiple rounds of dialogue,” thanks Shanghai AI Lab (including Bowen Zhou and the Intern team), and states that he “has independently verified all mathematical arguments and takes full responsibility for the manuscript.”
That is the author’s disclosure. It does not assign particular lemmas to the model line by line.
CGTN framed the story as a team led by Xu Disheng (Greater Bay University; visiting scholar at Shanghai AI Lab) working with Intern-S2, with the AI doing “large-scale, long-chain and highly complex mathematical derivations” while researchers steered direction. CGTN also called it “the first time Chinese scientists have relied on a domestically developed large AI model to crack a problem at this level.” “First time” and “world-class” are CGTN’s framing, not an independent ranking.
Zhang’s acknowledgements thank Xu for discussions and for facilitating his stay as a visiting scholar at Shanghai AI Lab when the main ideas took shape. The arXiv author list remains Zhang alone.
Lean formalisation
Zhang’s paper says Theorem A and Theorems 1.1, 1.2 and 1.3, plus Ghys results used in the paper, were formalised in Lean by the Bin Dong–Ruochuan Liu team at Peking University using the SHEAF formalisation agent, with formalisation work by Jiedong Jiang and Bin Wu. The repository is frenzymath/HolomorphicAnosov.
The README says those four theorems are proved with no sorry, that the Lean comparator accepts the solution, and that Theorems A, 1.1 and 1.3 take as a hypothesis HomotopyTorusRigidity — the torus case of the Borel conjecture, proved by Hsiang and Wall in 1969 — while Theorem 1.2 does not use it. So Lean is checking the encoded proofs under that classical assumption for three of the four statements.
CGTN said a Peking University team led by Liu Ruochuan and Dong Bin completed formal machine verification of the core theorems. Project-reported codebase sizes are not repeated here.
What remains open
- Peer review and acceptance by the mathematical community.
- How much of the creative proof work came from Intern-S2 versus the author.
- The conjecture “in higher dimensions” / higher codimension, which the paper itself says remains open in general.
Similar AI-math stories on TSN include DeepMind’s AlphaProof Nexus results in Science and OpenAI’s reported math and CS manuscripts. Those are separate events.
What this means
- A preprint, not a refereed theorem yet. The claim lives on arXiv and in Lean code the authors point to.
- AI as assistant, per the author. Zhang says Intern-S2 helped develop ideas; he says he verified every argument.
- Formal check is public. Readers can inspect the Lean targets and the Borel-torus hypothesis on GitHub.
Sources
- Jiesong Zhang, “Codimension-one holomorphic Anosov diffeomorphisms”, arXiv:2609.37695v3
- GitHub repository frenzymath/HolomorphicAnosov (Lean formalisation)
- CGTN, “Chinese researchers solve 3D Ghys conjecture with homegrown AI model”, 15 October 2026
Related stories
- Google DeepMind’s AlphaProof Nexus Is Published in Science: 9 of 353 Erdős Problems, 44 of 492 OEIS Conjectures, by the Authors’ Own Account
- OpenAI’s 372 math and CS results: Lean helps, independent checks pending
Follow @tsnmediahub on X for breaking AI news as it happens.
Follow on X
