Chinese AI Model Helps Prove Three-Dimensional Ghys Conjecture, With Lean Checking the Mathematics

A 1995 mathematics problem reaches a new milestone

A mathematical conjecture proposed in 1995 has yielded a proof covering complex dimension three, following a collaboration between mathematicians and Shanghai AI Laboratory's Intern-S2 model. A Peking University team then translated the paper's four main theorems into proofs checked by Lean, a computer system designed to verify mathematical reasoning.

Shanghai AI Laboratory announced the achievement on October 15, 2026, crediting a team led by Disheng Xu, a professor at Great Bay University and a visiting scholar at the laboratory. The research paper, Codimension-one holomorphic Anosov diffeomorphisms, lists Jiesong Zhang of Sweden's KTH Royal Institute of Technology as its sole author.

The result resolves the codimension-one case of French mathematician Etienne Ghys's conjecture, including the case in complex dimension three. It concerns a striking relationship between motion and shape: whether a space that supports a particular kind of chaotic motion must itself have a highly ordered mathematical structure.

Intern-S2 helped develop ideas and arguments through repeated exchanges with the researchers. Zhang states in his declaration of AI use that he independently verified all the mathematics. The collaboration combined machine exploration, human judgment and a separate process of formal verification.

The laboratory describes the achievement as the first use of a Chinese AI model to help solve a mathematical problem of this standing. The concrete result is a classification theorem, accompanied by a public preprint and publicly released formalization code.

What the proof says about motion and shape

Ghys's conjecture belongs to complex dynamics, the study of how mathematical systems change when their coordinates follow the rules of complex numbers. A complex number has two real components, so complex dimension three corresponds locally to six real dimensions. The setting is more abstract than an ordinary object moving through a room.

An Anosov system has a precise combination of stretching and squeezing. Under repeated motion, some directions contract while others expand. Nearby starting points can separate rapidly, producing chaotic behavior even though the rule governing every step is exact.

A useful picture is a repeated process that stretches and folds a shape. The mathematical system studied here is much more restrictive: its stretching and contraction must satisfy uniform conditions, and its motion must preserve the structure supplied by complex coordinates.

Ghys proposed that such systems on compact complex manifolds should have a standard algebraic description. A manifold is a space that looks simple in a small neighborhood, even when its complete shape is complicated. Compactness is a mathematical condition that, in this setting, keeps the space from extending indefinitely.

Zhang's theorem says that every codimension-one holomorphic Anosov diffeomorphism on a compact connected complex manifold is biholomorphically conjugate to a hyperbolic automorphism of a complex torus. In plainer language, a reversible change of coordinates that respects complex structure turns the motion into a standard algebraic transformation on a very regular space.

A complex torus can be constructed by identifying points in complex space that differ by elements of a repeating lattice. The central achievement is that the complicated dynamics force this orderly geometric description.

Why the precise scope matters

The paper addresses the codimension-one setting. For these systems, that means one of the contracting or expanding parts has complex dimension one. The theorem covers this restricted family in general and settles the conjecture in complex dimension three.

Ghys's broader conjecture concerns holomorphic Anosov systems across a wider range of complex manifolds and describes them using standard algebraic models on spaces called complex infra-nilmanifolds. Zhang's result supplies a particularly rigid answer for the case studied: a complex torus and a hyperbolic automorphism.

For mathematicians working on this case, the theorem changes the problem from identifying an unknown space and motion to studying a standard model. A change of coordinates connects the original system to that model while preserving the complex geometry.

Xu had spent years studying the problem. He previously investigated the case in dimension three with his former adviser, Fields Medal recipient Artur Avila. Xu and Zhang later obtained partial related results published in the Journal of the European Mathematical Society. The new work builds on that sustained attention to the same mathematical question.

From an Olympiad test to a research partnership

Intern-S2's role followed an earlier result by Intern-S1 in the 2025 Chinese Mathematical Olympiad. The Chinese Mathematical Society's committee responsible for secondary school mathematics competitions introduced an AI test that year, inviting three Chinese models to solve problems within the same time limit as human contestants.

Intern-S1 scored 102 points under the same marking standards, placing first among the three participating models. The gold medal threshold was 78 points, putting its score 24 points above that line, or about 31 percent higher.

Xu saw potential for using the model family in research mathematics, while Shanghai AI Laboratory wanted to move from competition problems to unresolved questions. Their collaboration began in early 2026 and included building a software system, described as a Harness, to organize the model's work and its exchanges with researchers.

The main stages were:

• 1995: Etienne Ghys proposed the conjecture.
• 2025: Intern-S1 scored 102 points in the Chinese Mathematical Olympiad AI test.
• Early 2026: Xu and Shanghai AI Laboratory began their model training collaboration.
• March 2026: Xu became a visiting scholar at the laboratory.
• August 2026: An internally developed version of Intern-S2 and its supporting system reached the stage used for intensive mathematical exploration.
• September 29: Zhang's paper was posted to arXiv, followed by a revision on October 13.
• October 15, 2026: The achievement was publicly announced.

How the mathematicians guided the AI

Intern-S2's first exploration of the problem produced a derivation report of about 400 pages. Xu invited Zhang, his former student and a postdoctoral researcher at KTH, to join the effort as a visiting scholar. Zhang had followed the Ghys conjecture since his doctoral studies.

Xu and Zhang examined the model's proposals, identified promising openings and supplied feedback to guide subsequent exploration. The machine pursued branches of reasoning and generated arguments; the mathematicians decided which directions deserved more work and helped assemble the final proof.

The laboratory describes seven batches of continued reasoning. During the process, the model's problem graph expanded from 15 nodes to 389, while the accumulated output reached roughly a thousand pages and included dozens of proposed approaches.

A problem graph is a map of smaller mathematical tasks and their connections. One node might represent an intermediate claim, while another represents a result needed to establish it. The reported increase shows how extensively the system divided and explored the problem.

Zhang's declaration of AI use gives a direct account of responsibility for the finished mathematics: an internal version of Intern-S2 helped develop the ideas and arguments through multiple rounds of dialogue, and he independently checked the mathematics. His paper also thanks Xu for continued discussions.

What the supporting software contributed

Shanghai AI Laboratory paired the model with software intended to manage long chains of reasoning and repeated human feedback. The system could split a difficult question into smaller tasks, explore several directions and return results for researchers to assess.

The training approach combined broad scientific knowledge with material aimed at research mathematics, including difficult problems drawn from mathematical papers and methods for checking proposed solutions. The laboratory also describes reinforcement learning using verifiable rewards, meaning that successful, checkable reasoning could provide a training signal.

Researchers then used experience from the supporting system to improve the model itself. The practical objective was to maintain useful progress across a long investigation, including tracking intermediate results and correcting mistakes as new arguments developed.

The laboratory also cited results on IMO-Proof and AdvancedMathBench, evaluations focused on mathematical reasoning. For the Ghys project, the most detailed evidence of how the system operated is the sequence of extensive derivations, expert feedback, a completed paper and subsequent formal verification.

How Peking University checked the proof

Peking University's team, led by Bin Dong and Ruochuan Liu, used its SHEAF framework to formalize all four main theorems in Zhang's paper. The work also covered results by Ghys on which the arguments depend.

Formalization translates mathematical definitions, assumptions and reasoning into a language a computer can check. A conventional paper can rely on a trained reader to fill in familiar steps. Lean requires those steps to be expressed through precise statements and permitted logical operations.

Team members Jiedong Jiang and Bin Wu said the effort took about five days, with as many as 100 AI agents operating in parallel. It produced approximately 550,000 lines of Lean code. Experts also checked that the formal statements matched the mathematical meaning of the paper's main theorems.

SHEAF organized the task as a directed graph of definitions, propositions and dependencies. This allowed different agents to work on connected pieces while the team tracked which statements had proofs and which still needed work.

The formalization required more than translating the final arguments. Some supporting results in dynamics were missing from existing formal mathematics libraries. The team had to supply that groundwork or find routes using results already available, then connect the pieces into a complete chain.

The paper is available as an arXiv preprint, and the formalization code has been released on GitHub. No journal publication or peer review decision was specified in the announcement.

Why the two stages belong together

Intern-S2 and SHEAF served different purposes. The first supported the search for mathematical ideas and arguments. The second helped construct formal proofs that Lean could check. Human mathematicians guided the exploration, checked the resulting mathematics and assessed whether the formal statements captured the intended theorems.

The scale of the work makes that division concrete. Roughly a thousand pages of exploratory output fed into a research paper; the verification process then generated about 550,000 lines of formal code. Each stage turned the work into a different form suited to a different task.

For future researchers, the public paper presents the mathematical argument, while the public code records the formal proof structure. The supporting definitions and results added during formalization may also provide starting points for later work in the same area.

The next step is a reusable verification module

Shanghai AI Laboratory plans to package the workflow as a mathematical verification module for its Intern Duanyan scientific discovery platform. The aim is to let later projects reuse the combination of model exploration, expert feedback and formal checking.

The laboratory also intends to apply the reasoning capabilities developed through this project to other disciplines with related mathematical structures. The proposed cycle is to solve a research problem, turn useful methods into reusable software and apply them to another investigation.

For Xu, the result extends a longstanding research interest through collaboration among Great Bay University, Shanghai AI Laboratory, KTH and Peking University. For the wider mathematical community, it offers both a new classification result and a detailed example of AI participating in research under human direction.

Key Points

• The new proof resolves the codimension-one case of the Ghys conjecture, including complex dimension three.
• Jiesong Zhang is the sole author of the research paper and says he independently verified all the mathematics.
• Disheng Xu and Zhang guided Intern-S2 through repeated exploration and feedback.
• The model's problem graph grew from 15 nodes to 389, with roughly a thousand pages of derivations.
• Peking University's SHEAF framework helped formalize four main theorems and supporting results in Lean.
• The verification effort reportedly took about five days and generated approximately 550,000 lines of code.
• The laboratory plans to turn the workflow into a reusable mathematical verification module.