For 31 years, the three-dimensional Ghys conjecture sat unresolved at the frontier of complex dynamical systems — elegantly stated, stubbornly resistant, open since Étienne Ghys first proposed it in 1995. On Wednesday, Shanghai Artificial Intelligence Laboratory announced that a team working closely with its Shusheng-S2 large model had finally closed the case, with an independent machine-verified formal proof in Lean certifying every logical step. The sole author of the underlying mathematical paper — postdoctoral researcher Jiesong Zhang of KTH Royal Institute of Technology in Stockholm — is 31 years younger than the problem he helped put to rest.

It is the first time a Chinese AI model has contributed to resolving a world-class open conjecture in pure mathematics, and it offers the most detailed account yet of what iterative human-machine collaboration on frontier research actually looks like in practice. It also raises a precise question the mathematics community has learned to demand of AI-assisted results: how do you know it is actually correct? In this case, the answer is unusually robust — and also unusually checkable by anyone with a Lean 4 installation.

The conjecture originates in a 1995 paper by Ghys, then at the École Normale Supérieure de Lyon, published in Inventiones Mathematicae under the title "Holomorphic Anosov systems." An Anosov diffeomorphism is a map on a manifold whose derivative simultaneously expands space in one family of directions and contracts it in another — a mathematical model of structured chaos, named after Soviet mathematician Dmitry Anosov and introduced in his 1967 work on diffeomorphisms.

What the Ghys Conjecture Says — and Why Three Dimensions Changed Everything

When that manifold also carries a complex-analytic structure and the diffeomorphism is holomorphic — meaning it respects the complex geometry — a strong rigidity is expected to appear. Ghys conjectured that this rigidity is total: every holomorphic Anosov diffeomorphism on a compact complex manifold should be biholomorphically conjugate to an affine automorphism of a complex infra-nilmanifold, the simplest possible algebraic model. The intuition is that complex structure leaves so little freedom for chaos that the only surviving maps must already come from linear algebra.

Ghys proved this for complex surfaces — the two-dimensional case. In three complex dimensions and beyond, the problem held out. The difficulty is concrete: a compact complex manifold topologically equivalent to a real torus is not necessarily a complex torus in dimension three or greater, because nonstandard complex structures exist on those underlying topological spaces. Ruling them out requires arguments that do not carry over from dimension two.

The new result, posted to arXiv in September as preprint 2609.37695 (submitted September 29, 2026; revised October 5, 2026), settles the codimension-one case — specifically, when one of the two characteristic sub-bundles of the map has complex dimension one. Because both sub-bundles must be nonzero, this covers all holomorphic Anosov diffeomorphisms on compact complex three-folds: the three-dimensional case the conjecture had named as its outstanding challenge since 1995.

Seven Cycles, 389 Nodes: How the AI-Human Proof Loop Worked

The team behind the proof was organized around Xu Disheng, a professor at Great Bay University in Dongguan who works as a visiting scholar at Shanghai AI Laboratory, and Jiesong Zhang, a postdoctoral researcher at KTH Royal Institute of Technology in Stockholm who completed his doctorate under Xu at Peking University. Zhang is the sole named author on the arXiv preprint; Xu's role was as academic supervisor and senior collaborator guiding the institutional partnership with Shanghai AI Lab.

Their approach centered on Shusheng-S2 and the lab's purpose-built "Harness system" — a platform Shanghai AI Lab designed to support large-scale recursive deduction and high-bandwidth human-machine interaction. Work began in August 2026 and proceeded through what the laboratory describes as a "general-specialized fusion" approach: the AI's broad reasoning capabilities were continuously calibrated by expert domain knowledge rather than operating independently.

In practice, this meant an iterative cycle of seven major rounds. In each round, Shusheng-S2 combed through relevant mathematical literature, decomposed the main proposition into sub-claims, explored multiple proof branches in parallel, checked logical consistency at each step, and rapidly tested candidate approaches. The AI generated thousands of pages of preliminary derivations and identified dozens of distinct mathematical approaches, many of which proved unworkable before a viable path emerged. Over the seven cycles, the proof graph — each node a mathematical claim or sub-result — expanded from 15 nodes to 389, according to Shanghai AI Lab's announcement of the result.

The human mathematicians were not passive monitors. After each cycle, Xu and Zhang reviewed outputs, identified which branches showed genuine analytical promise, and fed guidance back into the next round. The AI handled the combinatorial burden of hypothesis generation and step-by-step checking; the mathematicians supplied the strategic judgment that prevented the search from exhausting itself on dead ends.

According to Shanghai AI Laboratory's own announcement, reviewers familiar with the field noted the final proof exceeds the analytical depth that would have been anticipated from a purely human effort on this timeline. That claim originates with the laboratory and has not been independently assessed by outside reviewers in a public forum.

More Than 550,000 Lines of Lean Code Certify Every Step

An AI-assisted informal proof raises an immediate question that the mathematical community has increasingly demanded be answered: how do you know it is actually correct?

Here, the answer comes from a separate team entirely. Professors Dong Bin and Academician Liu Ruochuan at Peking University undertook a comprehensive formal verification of the proof using the Lean proof assistant and their proprietary SHEAF framework for complex dynamical systems.

Formal verification in Lean means something specific and demanding: every logical step in the proof is expressed in a machine-readable language and checked by a software proof kernel that certifies each inference follows from the axioms. There is no room for handwaving, no appeal to "it is clear that," no gap filled by a reader's intuition. A Lean proof either compiles — meaning every step is valid — or it does not.

The scope of the Peking University team's verification is substantial. Over approximately five days of continuous work, parallelized across up to 100 AI agents running simultaneously, the team generated more than 550,000 lines of Lean code. The verification confirmed the logical consistency of all four primary theorems underpinning the result. As a byproduct, it also established the first formal computer-verified infrastructure for the theory of complex dynamical systems — a field that previously had none.

Lean 4, the current version of the proof assistant, was created by mathematician and computer scientist Leonardo de Moura, originally at Microsoft Research and later at Amazon Web Services. The Lean Focused Research Organization (Lean FRO), a nonprofit, has maintained and developed the system since 2023. Lean's mathematical library, Mathlib, contained over 210,000 theorems and 100,000 definitions as of May 2025, including previous landmark verifications: a proof of Peter Scholze's "liquid tensor experiment" (2021) and Terence Tao's formalization of the Polynomial Freiman-Ruzsa conjecture (2023).

The Lean code from the Ghys verification is reported to be available on GitHub. Any mathematician with a Lean 4 installation can — in principle — attempt to compile it and reach the same conclusion the Peking University team did. That transparency is unusual and significant: the mathematical proof is more publicly auditable than the AI model that helped generate it.

Lean Verification Has Limits — Including One That Emerged in 2026

Lean verification does not make a result metaphysically infallible. The system certifies that a proof follows from its stated axioms within a particular formalization; it does not protect against axioms chosen incorrectly, against gaps between the informal mathematical claim and its Lean encoding, or against bugs in the proof kernel itself.

That last risk is not theoretical. In 2026, a researcher circulated what purported to be a Lean-verified disproof of the Collatz conjecture — one of mathematics' most famous open problems. The claim attracted substantial attention before an investigation found it rested on a bug in Lean's kernel; once the bug was corrected, the purported proof failed to compile. The episode illustrated that Lean verification is only as reliable as its underlying kernel, and that the kernel, however carefully maintained, is not immune to software defects.

For the Ghys conjecture verification, no such issue has been identified. But the 2026 incident provides appropriate context for calibrating confidence in formal proofs at scale, particularly when the Lean code runs to 550,000 lines — a volume that makes human line-by-line auditing impractical, leaving the community dependent on the kernel's correctness.

Shusheng-S2's Architecture and What Its Benchmarks Actually Show

Shusheng-S2 (书生大模型S2, also designated Intern-S2) is Shanghai AI Lab's flagship scientific multimodal large model, publicly released at the 19th Pujiang Innovation Forum in Shanghai on September 13, 2026. Its architecture centers on a Memory Decoder with pluggable professional knowledge modules, which allows domain-specific expertise to be incorporated without retraining the base weights — the mathematical corpus for this proof being one such module. The model was trained using advanced asynchronous long-horizon reasoning reinforcement learning, according to the lab's September 2026 release announcement.

The laboratory reports that on formal mathematics benchmarks — including IMO-Proof and AdvancedMathBench, which require rigorous step-by-step deduction rather than pattern recognition — Shusheng-S2 performs comparably to top closed-source models including Gemini 3.1 Pro.

Those benchmark figures come exclusively from Shanghai AI Laboratory itself and have not been independently verified by outside researchers. No published third-party evaluation of Shusheng-S2 on IMO-Proof, AdvancedMathBench, or equivalent formal reasoning benchmarks has appeared in the peer-reviewed or preprint literature as of this writing. The Ghys conjecture result is the first large-scale real-world evidence that Shusheng-S2's capabilities translate to genuine frontier research rather than competition problems whose solutions are already in training data — and it is meaningful evidence. But it does not substitute for independent benchmarking.

The laboratory documentation also notes that Xu Disheng's team's ongoing mathematical research helped inform and improve Shusheng-S2 during its development — a closed loop the lab describes as AI being built collaboratively with scientists. That relationship makes the Ghys result a proof of methodology as much as a proof of the conjecture: evidence for the iterative "general-specialized fusion" approach that the lab intends to package into its Shusheng-Duanyan (书生·端言) scientific discovery platform.

Can Researchers Outside China Reproduce or Access This Work?

The Lean code is reportedly available on GitHub, making the formal verification side of the result reproducible in principle by any researcher with a Lean 4 installation, a modern workstation, and time.

The AI-assisted proof generation is a different matter. Shusheng-S2 is not available through a public API or a hosted service accessible to international researchers for independent benchmarking or replication. The Harness system, the proprietary platform that orchestrated the iterative proof cycles, is similarly inaccessible outside Shanghai AI Lab.

This creates an asymmetry at the heart of the result. The mathematical claim — the 3D Ghys conjecture — is now as rigorously verified as any theorem in mathematics, because the Lean code that certifies it is public. The AI methodology that produced the informal proof cannot be independently evaluated, because the model and its infrastructure are not. A researcher who wants to apply the same approach to a different conjecture cannot download Shusheng-S2, access the Harness system, or reproduce the iterative collaboration as described.

Jeremy Avigad, a Carnegie Mellon University logician who has been closely involved in Lean's development, has written that AI-assisted formal proofs in Lean represent significant advances in the field. Terence Tao, the UCLA mathematician and Fields medalist, has offered a more cautious read of the broader trend: AI systems that generate mathematical results at scale risk leaving mathematical fields less fertile for future human discovery. Daniel Litt of the University of Toronto has suggested the community should approach AI-generated proofs as inputs to be checked and understood rather than conclusions to be accepted.

None of these researchers have commented specifically on the Ghys conjecture result. Their views reflect the community's evolving framework for evaluating a class of claims to which this result belongs.

Three Chinese Laws Make Shanghai AI Lab's Research Subject to Government Access

Shanghai AI Laboratory is a Chinese state-backed nonprofit, founded in July 2020 with support from the Shanghai municipal government and national science agencies. It operates as part of China's "national team" for artificial intelligence under the 14th Five-Year Plan.

As a Chinese legal entity, the laboratory — and its research outputs, communications, model weights, and data — is subject to three laws that carry mandatory government cooperation requirements regardless of the institution's nonprofit status or academic orientation:

China's National Intelligence Law (2017), Article 7 requires that "all organizations and citizens shall support, assist, and cooperate with national intelligence work in accordance with the law." This obligation applies to Shanghai AI Lab as an organization and to its personnel as citizens. It is not conditional on the nature of the work being conducted.

China's Data Security Law (2021) governs data processing activities within China, requires security reviews for "important data," and subjects data processors to government access on demand. China's Cybersecurity Law (2017) requires network operators to store data within China and to cooperate with law enforcement and intelligence agencies.

These obligations are fixed legal conditions of operating under Chinese jurisdiction. They apply regardless of the laboratory's stated privacy policies, the physical location of its servers, or any statements by laboratory personnel about government independence. Researchers and institutions considering formal collaboration with Shanghai AI Lab, or use of its research outputs in sensitive applications, should factor these obligations into their assessment.

Xu Disheng, the visiting scholar who led the Shanghai AI Lab side of the collaboration, holds his primary position at Great Bay University in Dongguan — a research institution that received government approval in June 2025 and began operations in late 2025. Zhang Jiesong, the sole arXiv author, is based at KTH Royal Institute of Technology in Stockholm, Sweden, outside Chinese jurisdiction.

What Comes Next for AI-Assisted Mathematical Discovery

The breakthrough fits into a changing landscape for AI and mathematics. In 2025 and 2026, systems from OpenAI, Google DeepMind, and other Western labs demonstrated that large models can contribute to graduate- and research-level mathematics, including resolving longstanding open problems at a pace that has alarmed some mathematicians. What distinguishes the Ghys conjecture result is the combination of genuine open-problem status, a multi-month iterative human-AI collaboration documented in detail, and a completed machine-verified formal proof — elements that few prior claims of AI-assisted mathematical discovery can all point to simultaneously.

The Peking University verification team's work also produced something of lasting value to the field independent of the Ghys result itself: the SHEAF framework, described as the first formal Lean infrastructure for the theory of complex dynamical systems. Any future mathematical work in this domain can now build on a machine-verified foundation rather than starting from scratch.

Shanghai AI Lab says it intends to extend the methodology — the Harness system, the iterative human-machine cycle, and the Lean formalization pipeline — to its Shusheng-Duanyan scientific discovery platform, connecting AI reasoning with experimental devices and data infrastructure across life sciences, materials science, and quantum computing.

For the mathematics community, the 3D Ghys conjecture closes a chapter open since 1995. For the AI research community, the more pressing question may be whether a methodology this effective — and this difficult to independently verify on the AI side — will be widely adopted, selectively used, or viewed with the caution that Tao and Litt have counseled.

Frequently Asked Questions

What is the Ghys conjecture, and why did it take 31 years to prove?

The Ghys conjecture, proposed in Étienne Ghys's 1995 paper "Holomorphic Anosov systems," asserts that every holomorphic Anosov diffeomorphism on a compact complex manifold must be biholomorphically conjugate to an affine automorphism of a complex infra-nilmanifold — in plain terms, that complex geometry constrains this class of dynamical systems so tightly that only the simplest algebraic models can survive.

Ghys proved the two-dimensional version himself. The three-dimensional case required ruling out exotic complex structures that don't exist in two dimensions, and the tools for doing so didn't come together until Jiesong Zhang, working with Shusheng-S2 over seven iterative cycles across months of collaboration, traced a complete proof path through 389 nodes the AI helped construct.

What does machine-verified formal verification in Lean actually mean, and can anyone check it?

Formal verification in Lean means every logical inference in the proof is expressed in a machine-readable programming language and validated by a software proof kernel that certifies each step follows from the axioms. A proof that compiles in Lean has been checked mechanically; there is no room for the informal leaps that occasionally go unnoticed in peer-reviewed mathematics. The 550,000-line Lean code from the Peking University team is reported to be available on Lean 4's GitHub repository. Any researcher with a Lean 4 installation can — in principle — attempt to compile it. The caveat: in 2026, a Lean kernel bug briefly allowed a false Collatz disproof to appear valid; the bug was found and fixed, but it illustrates that Lean verification is only as reliable as its kernel.

Can researchers outside China access Shusheng-S2 or the Harness system to replicate this work?

Not currently. Shusheng-S2 is not available through a public API or hosted service accessible to international researchers, and the Harness system — Shanghai AI Lab's proprietary platform for large-scale recursive deduction — has not been released publicly. The mathematical claim is fully verifiable by anyone who can compile the Lean code; the AI methodology that helped discover the informal proof cannot be independently replicated or benchmarked. This asymmetry is worth understanding clearly: the theorem is as well-verified as any in modern mathematics, but the tool that helped find it remains a black box outside Shanghai AI Lab's walls.

Does this mean AI can now prove any major unsolved mathematics problem?

No — and several prominent mathematicians have cautioned against reading results like this one as evidence that AI is on the verge of exhausting open mathematics. Terence Tao has warned that AI systems generating mathematical results at scale risk leaving entire fields less fertile for future discovery. Daniel Litt has suggested treating AI-generated proofs as inputs to be checked and understood rather than settled conclusions. The Ghys conjecture result is evidence that iterative human-AI collaboration, disciplined by expert review and anchored by formal verification, can close specific frontier problems. It is not evidence of autonomous mathematical intelligence.