A preprint credits an internal Intern-S2 with help on a Ghys case, then Lean

On 15 October 2026, Shanghai Artificial Intelligence Laboratory published a news note whose headline says Chinese scientists have, for the first time, used a Chinese large model to crack a world-class mathematics problem. That “first” is the laboratory’s framing. The note says a team led by Xu Disheng, a professor at Great Bay University and a visiting scholar at the laboratory, used the lab’s Intern-S2 model (Shusheng-S2, 书生-S2) in a human-AI collaboration to prove the three-dimensional Ghys conjecture, and that a Peking University team led by Dong Bin and Liu Ruochuan then formalized the four main theorems in Lean with its SHEAF framework.

The preprint the note names is public, and so is a Lean repository. They do not say all of what the news note says.

What Ghys’s conjecture is, in the paper

Codimension-one holomorphic Anosov diffeomorphisms, by Jiesong Zhang, quotes the conjecture from Étienne Ghys, “Holomorphic Anosov systems,” Inventiones Mathematicae 119 (1995). In the paper’s words, Ghys proposed that every holomorphic Anosov diffeomorphism is biholomorphically conjugate to an affine automorphism of a complex infra-nilmanifold. Ghys verified that for complex surfaces. An Anosov diffeomorphism, as the introduction sets it up, is a smooth map of a compact manifold whose tangent space splits into steadily contracted directions and steadily expanded ones.

The abstract says the paper proves that every codimension-one holomorphic Anosov diffeomorphism of a compact connected complex manifold is biholomorphically conjugate to a hyperbolic automorphism of a complex torus. It says this verifies Ghys’s conjecture in the codimension-one case and, in particular, in complex dimension three. The three-dimensional case is the one the laboratory’s headline names. The theorem Zhang states is the codimension-one case, which includes dimension three because, as the paper notes, both invariant distributions are nonzero there, so one of them has complex dimension one.

The arXiv record lists a single author, Jiesong Zhang. Version 3, updated 13 October 2026, is 19 pages. The first version date on the abstract page is 29 September 2026. The comment on version 3 says it adds a declaration of AI use, a statement on proof formalisation, and acknowledgements.

What the author says the model did

The declaration says the author used an internal version of Intern-S2 to assist in developing the mathematical ideas and arguments, through multiple rounds of dialogue. He writes that he has independently verified all mathematical arguments and takes full responsibility for the manuscript. He thanks Shanghai AI Lab, Bowen Zhou, and the Intern team.

The acknowledgements say the question was already under consideration while Zhang and Disheng Xu were finishing a joint paper, and that Xu continued the discussions and facilitated Zhang’s stay as a visiting scholar at the laboratory, “when the main ideas of this work took shape.” Xu is thanked. He is not an author on the preprint. The laboratory’s note describes a larger collaboration, with Xu leading and Zhang joining as a visiting scholar, and it describes multi-round exploration, a 400-page first report, and later output it calls about a thousand pages. Those production details are in the news note. They are not in the preprint.

The paper thanks Junyi Xie for comments on the problem and on the first version. The news note goes further and says Xie tried GPT-6 on the problem and did not solve it. That trial is the laboratory’s anecdote. It is not in the paper. No separate public comment from a mathematician outside this paper and this news note turned up in the searches opened for this story.

The paper says the work was supported in part by national program 2024YFA1015100 and by NSFC grants 12090010 and 12090015. The laboratory is a Shanghai research institute publishing this result as its own news.

What the Lean repository actually checks

The paper’s formalisation note says Theorem A and Theorems 1.1, 1.2, and 1.3, together with the Ghys results the paper uses, were formalized in Lean by the Bin Dong and Ruochuan Liu team at Peking University, using SHEAF. It names Jiedong Jiang and Bin Wu as the people who carried out the formalisation, including human verification of the final theorem. The code is frenzymath/HolomorphicAnosov. GitHub records that repository as created 13 October 2026. The README says the four theorems are proved with no sorry, using only the axioms propext, Classical.choice, and Quot.sound, modulo one hypothesis: Theorems A, 1.1, and 1.3 take HomotopyTorusRigidity, the claim that for dimension at least 5 every closed smooth manifold homotopy-equivalent to a torus is homeomorphic to it. The README identifies that as the Borel conjecture for tori, proved by Hsiang and Wall in 1969, and says it is a hypothesis of the statements, not a Lean axiom, and that Theorem 1.2 does not use it. The toolchain line is Lean v4.35.0-rc1. The repository has no LICENSE file. GitHub’s license API returns none.

The laboratory says Jiang and Wu described the formalisation as about five days, with up to 100 agents running at once, producing about 550,000 lines of Lean. The paper and the README do not give those three figures. They are the news note’s account of what those two researchers said.

Same-day headlines on Phoenix and Pandaily were requested on 15 October. Neither page returned article text, so no figure here is taken from them.

What is public is Zhang’s 19-page preprint, an AI-use declaration about an internal Intern-S2, and a Lean development that checks four theorems while leaving a 1969 torus result as a hypothesis. The arXiv page does not claim peer review. The laboratory’s “first time” sentence is the laboratory’s.