Intern-S2 helps prove Ghys's conjecture in complex dimension three, checked in Lean

What was proved

Shanghai AI Laboratory said on 15 October 2026 that mathematicians working with its Intern-S2 model have resolved Ghys's conjecture in complex dimension three, a question in dynamical systems that has been open since 1995. The result is a 19-page preprint, Codimension-one holomorphic Anosov diffeomorphisms, by Jiesong Zhang of KTH Royal Institute of Technology in Stockholm, who is listed as its only author.

The main theorem says that every codimension-one holomorphic Anosov diffeomorphism of a compact connected complex manifold is biholomorphically conjugate to a hyperbolic automorphism of a complex torus. Put more simply: if a smooth, complex-analytic map stretches space in one direction and squeezes it in the others in a very regular way, the space it acts on has to be a complex torus, and the map has to be, after a change of coordinates, one of the standard linear examples. Because in three complex dimensions one of the two directions must be one-dimensional, the codimension-one case covers all of dimension three.

A team at Peking University then checked the paper's four main theorems in Lean, a proof assistant that verifies formal proofs line by line, and published the code in a public HolomorphicAnosov repository. Shanghai AI Lab's announcement frames the work as a step for AI-assisted research mathematics, with the model doing large-scale exploration and the mathematicians deciding what was worth keeping.

Why Ghys's conjecture is hard

Anosov systems are a classic source of chaos. Nearby points are pulled apart exponentially fast along one set of directions and pushed together along another, so trajectories that start close end up far apart. Shanghai AI Lab's announcement illustrates the idea with the cat map, a simple stretching rule on a square, while noting that it is not one of the holomorphic systems in the paper.

In 1995 the French mathematician Étienne Ghys proposed that when such a system also respects a complex structure, the geometry is forced. His conjecture says every holomorphic Anosov diffeomorphism is biholomorphically conjugate to an affine automorphism of a complex infra-nilmanifold. Ghys proved it for complex surfaces. Later work by Cantat settled projective manifolds under extra assumptions, and other work classified systems that are bi-Lipschitz conjugate to affine models, as the new paper recounts.

The new paper's route has two steps. First it shows the manifold is a torus and the map is topologically conjugate to a hyperbolic toral automorphism, removing a transitivity assumption from one of Ghys's own theorems by building a linearisation of the stable leaves. Then it upgrades that to a holomorphic conjugacy, which is harder than it sounds because a complex manifold that is topologically a torus need not carry the standard complex structure. The conjecture remains open in higher dimensions in general.

How Intern-S2 was used

Shanghai AI Lab gives a detailed account of the collaboration. Disheng Xu, a professor at Great Bay University and a visiting scholar at the lab, had studied the three-dimensional case with his doctoral adviser, the Fields Medallist Artur Avila, without finding a proof strategy. Xu and Zhang later published related results in the Journal of the European Mathematical Society.

The lab says joint research with the Intern team began in early 2026, after its earlier Intern-S1 model scored 102 points in an official AI evaluation at the 2025 Chinese Mathematical Olympiad finals, above the human gold-medal threshold of 78. Intern-S2 is the lab's multimodal model for scientific research, combining broad scientific pretraining with specialised training on research mathematics and reinforcement learning for long reasoning sequences.

Starting in August 2026, Intern-S2 and a supporting system explored the conjecture from several directions. The first round produced a report of roughly 400 pages of candidate arguments. Xu and Zhang found a promising opening in it, then used repeated dialogue to test, redirect and develop the ideas. Across seven rounds, the lab says, the system's problem graph grew from 15 to 389 nodes and produced about a thousand pages of working material and dozens of possible lines of argument. The lab describes these outputs as intermediate material that the mathematicians had to assess, refine and connect into a proof. These process figures are the lab's own and have not been independently audited.

What the Lean check covers

The formal check was carried out by Jiedong Jiang and Bin Wu in the team of Bin Dong and Ruochuan Liu at Peking University, using their open-source SHEAF framework. SHEAF breaks a paper into a dependency graph of statements and lets coding agents such as Claude Code or Codex fill in Lean proofs from the target theorems downwards, skipping anything the final proofs do not use. The lab reports that the job took about five days, with up to 100 agents working at once, and produced roughly 550,000 lines of Lean.

According to the repository, Theorem A and Theorems 1.1, 1.2 and 1.3 are proved with no unfinished steps, using only Lean's three standard axioms, and the Lean comparator tool accepts the proofs against a separate file that states the theorems using only the Mathlib library. Shanghai AI Lab adds that experts checked that the formal statements match the claims in the paper, which matters, because a formal proof is only as good as the statement it proves.

There is one stated input. Theorems A, 1.1 and 1.3 take as a hypothesis the rigidity of homotopy tori, the fact that in dimension five and up a closed smooth manifold homotopy equivalent to a torus is homeomorphic to it. W.-C. Hsiang and C. T. C. Wall proved that in 1969. It is a classical theorem rather than a gap, but it was assumed in Lean, not formalised. Theorem 1.2 does not need it.

What the paper itself says about AI

The arXiv record shows the paper first went up on 29 September 2026 and was revised on 5 and 13 October. The third version added a declaration of AI use, a statement on the formalisation and acknowledgements. In it Zhang writes that 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." He adds that he "has independently verified all mathematical arguments and takes full responsibility for the manuscript."

That wording is narrower than some coverage. China's state broadcaster CGTN described the result as the first time Chinese scientists relied on a domestically developed large AI model to crack a problem at this level. The paper does not say which lemmas came from the model, and, as Frontier Now pointed out, its declaration cannot by itself apportion credit between the model and the mathematicians. The model used was an internal version, so outsiders cannot rerun the exploration with the same system.

Where this sits in AI-assisted maths

The announcement lands in a busy month for machine-assisted mathematics. Google DeepMind published AlphaProof Nexus in Science after it solved nine open Erdős problems, and OpenAI released 722 AI-written math manuscripts with Lean artifacts, several of which were later revised or withdrawn. OpenAI and Anthropic have also joined a $15 million Simons Foundation fund for checking AI maths.

This case differs in shape. It is a single named conjecture, one human author who signs for the result, a model described as a collaborator rather than an autonomous prover, and a formal check done by a separate team with agents. That division of labour, with the model widening the search, humans choosing the path and a proof assistant checking the end product, is the workflow several labs have been describing, here applied to a problem that specialists had worked on for decades.

What it means for researchers

For mathematicians, the practical lesson is about verification rather than discovery. A model that produces hundreds of pages of candidate arguments is only useful if experts can sift them, and the Lean step gives referees something they can rerun. The repository includes the commands to build the library and run the comparator, though it needs a release-candidate Lean toolchain and some extra tools.

Shanghai AI Lab says its next step is to package the workflow as a reusable mathematics verification module in its scientific discovery platform and to try the reasoning methods on problems with related structure in other fields. SHEAF is already public, and its own documentation reports that in an earlier formalisation 62.5% of the planned nodes not already in Mathlib turned out not to be needed, which is where much of its speed comes from.

Limits and open questions

The paper is a preprint and has not been peer reviewed. The Lean check is strong evidence that the four theorems follow from their stated hypotheses, but it relies on the statements being faithful to the mathematics, on the Hsiang-Wall input, and on Mathlib's existing definitions. The HolomorphicAnosov repository, created on 13 October, had no licence file when AI Lookout checked it.

It is also unclear how much of Intern-S2's contribution would transfer to other problems, what the internal model costs to run, or when, if ever, that version will be released. The real-number version of the question, and Ghys's conjecture in higher complex dimensions, remain open. AI Lookout did not rerun the Lean build.