Shanghai AI Lab’s Intern-S2 Helped Prove Ghys’s Codimension-One Holomorphic Anosov Conjecture
A new arXiv preprint credits an internal Intern-S2 science model with helping develop a proof of Étienne Ghys’s 1995 conjecture in the codimension-one case; main theorems were formalized in Lean by a Peking University team.
By 1EyeAI Desk ·
Shanghai Artificial Intelligence Laboratory said on Oct. 15, 2026 that researchers working with its Intern-S2 (书生-S2) science model helped prove the codimension-one case of Ghys’s conjecture on holomorphic Anosov diffeomorphisms—a problem Étienne Ghys posed in 1995. The lab’s announcement frames it as human–machine collaboration; state outlets including CGTN and the Global Times repeated that framing.
The primary mathematical claim is on arXiv as arXiv:2609.37695, “Codimension-one holomorphic Anosov diffeomorphisms,” sole author Jiesong Zhang (KTH). The abstract says every such diffeomorphism on a compact connected complex manifold is biholomorphically conjugate to a hyperbolic automorphism of a complex torus, verifying Ghys’s conjecture in the codimension-one case and, in particular, in complex dimension three. In the paper’s Declaration of AI Use, Zhang writes that he used an internal Intern-S2 “to assist in developing the mathematical ideas and arguments… through multiple rounds of dialogue,” thanks Shanghai AI Lab, and states that he “has independently verified all mathematical arguments and takes full responsibility for the manuscript.”
Zhang also notes that Theorem A and Theorems 1.1–1.3, plus Ghys results used in the paper, were formalized in Lean by the Bin Dong–Ruochuan Liu team at Peking University with the open-source SHEAF agent; code is at github.com/frenzymath/HolomorphicAnosov. Shanghai AI Lab’s post claims process details such as a ~400-page first derivation report, seven reasoning rounds, and a problem graph grown from 15 to 389 nodes; those figures are project-reported, not independently audited.
This remains a preprint, not a journal-refereed theorem. Formal Lean checks of the stated main theorems are a strong public signal, but peer review and community scrutiny of the paper and the formalization targets still matter. Lab and state-media lines that call it the “first” Chinese LLM to crack a “world-class” problem are their framing, not an independent ranking.
What this means for you: If you follow AI-for-math, treat this as a documented assist-and-formalize case study: read Zhang’s AI declaration, the abstract, and the Lean repo. If you only use consumer chatbots, nothing changes in your apps today.