Intern-S2 Helps Prove the Three-Dimensional Ghys Conjecture, Verified via Formalization

The team of Professor Xu Disheng, a visiting scholar at Shanghai AI Laboratory and professor at Greater Bay Area University, has completed a proof of the three-dimensional Ghys conjecture through human-machine collaboration, relying on the Intern Science Multimodal Large Model S2 (Intern-S2). The team of Professor Dong Bin and Academician Liu Ruochuan at Peking University used their independently developed SHEAF framework to formally verify the proof, confirming its rigorous correctness. Some in the industry believe this marks the first time Chinese scientists have used a Chinese large model to conquer a world-class mathematical problem.

The related paper has been published on the preprint platform arXiv, and the formalization code has also been made public on GitHub.

The Ghys Conjecture: Finding the Geometric "Underlying Code" for Chaotic Dynamical Systems

The Ghys conjecture was proposed by French mathematician Étienne Ghys in 1995. Its core question is: whether the existence of chaotic dynamical system behavior can determine geometric classification. This is an important hard problem in the field of complex dynamics. If the conjecture holds, chaotic dynamical trajectories can be "reduced" to simple, regular standard algebraic models.

How to understand this intuitively? Imagine a "world" that is closed and finite, without boundary, where every small patch follows the rules of complex arithmetic. For Anosov systems, one can use the analogy of kneading dough: pressing, stretching, and folding dough, with some directions being stretched and others compressed. The stretching effect causes initially adjacent points to rapidly separate—tiny differences in initial conditions lead to completely different evolutionary outcomes.

The Ghys conjecture says that as long as there exists such a motion that is "both like kneading dough and completely regular," then this "world" can only be a shape that is repeatedly assembled from simple rules, highly regular like a crystal lattice, such as a complex torus. In other words, this motion is essentially just a simple translation, rotation, or scaling of that "world." If the motion is too chaotic, it will in turn determine what shape the world can only take.

Professor Xie Junyi, a 45-minute speaker at the 2026 International Congress of Mathematicians and a professor at Peking University's Beijing International Center for Mathematical Research, commented: "The difficulty of the Ghys conjecture lies in the fact that the analogous assertion in its corresponding real version is still a famous, completely open hard problem. The complex case makes the problem more rigid, and it is an important problem in the study of rigidity phenomena in complex dynamics, extremely difficult."

Professor Xu Disheng of Greater Bay Area University has long been deeply engaged with this conjecture. He once collaborated with his advisor, Fields Medalist Professor Artur Avila, on the three-dimensional case, but did not form an effective proof approach; afterward, he collaborated with his student Dr. Zhang Jiesong and obtained some weakly related partial results on the Ghys conjecture in the three-dimensional case, with the related results published in the top mathematics journal Journal of the European Mathematical Society (JEMS).

Complex dynamics is a branch of mathematics that studies the iteration behavior of holomorphic (or meromorphic) maps on the complex plane. Its core objects include Julia sets, Fatou sets, and the Mandelbrot set. Compared with dynamical systems over the real numbers, complex analyticity endows the system with extremely strong rigidity—the structure of the map is strictly constrained by the properties of analytic functions, and small perturbations often lead to drastic changes in overall behavior. Anosov systems are a special class of systems in differentiable dynamical systems, whose tangent bundle can be decomposed into two subspaces of uniform expansion and uniform contraction. Typical examples include linear hyperbolic automorphisms on tori. A complex torus can be understood as the space obtained by taking the quotient of an n-dimensional vector space over the complex numbers by some lattice (a discrete additive subgroup). It carries a complex structure with a translation group and is one of the simplest compact complex manifolds.

Anosov (Dmitri Anosov, 1936–2022) was a Soviet mathematician who systematically studied hyperbolic dynamical systems around 1967; such systems were later named Anosov systems. A complex torus is a compact complex manifold of the form ℂⁿ/Λ, where Λ is a lattice of rank 2n. It is a higher-dimensional generalization of compact Riemann surfaces (for n=1, elliptic curves), and also the most basic model in the intersection of algebraic geometry, complex geometry, and dynamical systems.

Seven Batches of Successive Deduction, 389 Nodes: A Key Breakthrough Through Human-Machine Collaboration

Zhou Bowen, Director and Chief Scientist of Shanghai AI Laboratory, has a judgment: the older and more fundamental the problem, the greater the room for AI to improve efficiency. Monoclonal antibodies, protein folding, and the still-unresolved Millennium Prize Problem, the Navier–Stokes equations, all fit this pattern. The three-dimensional Ghys conjecture is precisely one of these fundamental hard problems.

In March 2026, Professor Xu Disheng became a visiting scholar at Shanghai AI Laboratory. The two sides formed a joint team and simultaneously built a Harness system oriented toward mathematical research scenarios. Combining his experience in mathematical research, Professor Xu Disheng precisely pointed out the capability shortcomings of the model and system; relying on real frontier mathematical research problems, he drove the system through multiple rounds of iterative refinement.

In August 2026, the internally iterated Intern-S2 and its supporting system possessed large-scale recursive reasoning capabilities and highly flexible human-machine interaction capabilities. For the first round of reasoning on the three-dimensional Ghys conjecture, Intern-S2 produced a 400-page derivation report.

At the training strategy level, the research team adhered to the "general-purpose and specialized integration" technical route. On the basis of consolidating the model foundation through large-scale scientific knowledge pretraining, they carefully constructed research-level post-training data, including large-scale hard problems from mathematics papers and reliable verification schemes, to improve the model's professionalism, rigor, and standardization in research-level mathematics. At the training algorithm level, the team broke through asynchronous long-horizon reasoning reinforcement learning training methods, solving a series of fundamental problems under verifiable rewards, such as exponential accumulation of errors, long-term state maintenance, and self-correction; they also developed a self-evolution algorithm that reverse-distills improvements in Harness capabilities back into the model.

On competition mathematics and advanced mathematics benchmarks that emphasize long-horizon rigorous reasoning, such as IMO-Proof and AdvancedMathBench, Intern-S2 overall leads existing open-source models and surpasses top closed-source models such as Gemini 3.1 Pro on some metrics.

The key to the breakthrough lies in closer human-machine collaboration: Intern-S2 and its supporting system leverage the advantage of long-chain large-scale deduction, spreading out multiple branches for simultaneous attempts, decomposing complex propositions, and conjecturing different ideas; researchers are responsible for grasping the overall direction, judging which ideas are worth exploring in depth, which paths are dead ends, and providing intuitive suggestions. The two iterate through multiple rounds of dialogue and feedback.

Building on the first round of exploration given by AI, Xu Disheng and Zhang Jiesong keenly seized the key breakthrough point, continuously giving feedback to the model and calibrating the direction of exploration. During the research process, Intern-S2 completed seven batches of successive deduction, with the problem graph expanding from 15 nodes to 389 nodes, outputting a total of over a thousand pages of rigorous derivation, while also generating dozens of entirely new lines of argument.

An intriguing detail: before the paper was uploaded to arXiv, dynamical systems expert Professor Xie Junyi had also used GPT-6 to attempt this problem and did not find a proof. This indirectly confirms the unique value of Intern-S2 in this frontier mathematical exploration, and also sends a signal—China's large models are equally capable of standing on the field of frontier mathematics.

General-purpose and specialized integration refers to layering domain-specific post-training data and algorithms on top of a general foundation model, so that the model retains general reasoning ability while achieving expert-level performance in a specific professional field. The traditional route often involves a trade-off between "general" and "specialized": general models have broad knowledge but lack professional depth, while specialized models have high precision but poor generalization; general-purpose and specialized integration attempts to inject professional capabilities while retaining the general foundation through a combination of continued pretraining, instruction fine-tuning, and reinforcement learning. In mathematical research, this means the model must not only understand everyday language, but also master a rigorous mathematical symbolic system, proof conventions, and paper citation habits.

Asynchronous long-horizon reasoning reinforcement learning refers to splitting long-chain reasoning into multiple branches that can be advanced in parallel and interleaved, and training with reinforcement learning under asynchronous scheduling. Its difficulties lie in: as the number of reasoning steps increases, numerical errors and logical deviations accumulate exponentially; long-term states (such as already-proved propositions and assumption conditions) are difficult to maintain stably; and the model also needs self-correction capability. Verifiable rewards are especially important in such tasks—each step of a mathematical proof can provide deterministic feedback through a formal system or human review, thereby providing a stable signal for reinforcement learning.

Peking University Team's SHEAF Framework Completes Formal Verification

Can the results produced with AI assistance withstand verification? The team of Professor Dong Bin and Academician Liu Ruochuan at Peking University completed the formal verification of all four main theorems of this paper, and the proof has passed Lean checking. As an interactive theorem proving system, Lean can perform strict logical checks on formal proofs.

Jiang Jiedong and Wu Bin, key members of the Peking University team, introduced that the entire process took only about 5 days, with peak concurrency reaching 100 agents and producing about 550,000 lines of Lean code. Experts confirmed that the formal statements are semantically consistent with the paper's main theorems, and the Lean verification accordingly ensures their rigorous correctness.

The difficulty of formalization first comes from mathematics itself: natural-language proofs often rely on the reader's mathematical knowledge to fill in conditions and reasoning, while formalization must implement them as a complete proof checkable by computer. If results cited in the paper have not entered the foundational theorem library, one must supplement formal proofs or find alternative routes using existing results. The field of dynamical systems originally lacked sufficient formalization infrastructure; this work supplemented a large amount of infrastructure, covering many literature results on which the paper depends.

To organize this process, the Peking University team used the independently developed SHEAF framework: multiple agents organize the propositions, definitions, and dependency relations in the paper into a directed acyclic graph extending layer by layer from the target theorem to the foundational theorem library; under the framework, the model participates in proposition decomposition and formal proof construction, and the team orchestrates work around this graph, tracking the statement, proof, and pruning status of each node, decomposing large-scale formalization tasks into interconnected, checkable steps.

The Peking University mathematics team is one of the earliest research teams in the world to lay out the AI for Math direction, building a complete technical chain covering high-difficulty evaluation sets (FATE), large-scale mathematical knowledge retrieval (Matlas/LeanSearch), and automated reasoning and formal verification (Rethlas/Archon/Danus/Iteris). Its developed AI system previously successfully tackled the Anderson conjecture, and recently also independently completed the formal verification of the Poincaré conjecture.

Lean is an interactive theorem prover initiated and continuously developed by Microsoft Research. It is based on the Calculus of Constructions, a dependent type theory. Users can write mathematical definitions, theorems, and proofs in it, and the system checks step by step whether each step is legal. Lean's mathematics library, mathlib, has accumulated hundreds of thousands of theorems, covering algebra, analysis, topology, algebraic geometry, and other fields, and is one of the most important infrastructures for formal verification in AI for Math today. The core value of formal verification lies in this: it transforms "humans believe it is correct" into "machines can mechanically check rigorous correctness," thereby eliminating implicit assumptions and skipped steps in natural-language proofs.

SHEAF is an agent framework developed by the Peking University team for large-scale mathematical formalization. Its design idea is to organize the propositions, definitions, lemmas, and their dependencies in a paper into a directed acyclic graph (DAG), with the bottom nodes of the graph corresponding to existing foundational theorems in the Lean mathematics library and the top nodes corresponding to the main theorem to be proved. Multiple agents divide labor around this graph: some are responsible for translating natural-language propositions into Lean statements, some attempt to construct proofs, and some are responsible for pruning and backtracking when a branch fails. This "graph orchestration + agent parallelism" approach enables formalization work that originally required person-months to be completed in a few days, and also provides a scalable engineering path for verifying AI-generated mathematical proofs.

From Solving a Single Hard Problem to Research Infrastructure

The significance of this research goes beyond the proof of one conjecture. Traditional mathematical research relies on the long exploration of individual geniuses, whereas this effort systematically connects expert intuition into the machine solving loop, forming a closed loop of "systematic exploration—expert judgment—accumulation of results—feedback correction."

This paradigm can be replicated and extended to more fundamental research fields with "huge search spaces and scarce experts," enabling more "from 0 to 1" original innovation breakthroughs.

Next, building on the complete capability loop proven in this research, the team will further encapsulate it into reusable mathematical verification modules for the Intern·Duanyan scientific discovery platform, to be directly invoked in subsequent scientific research. At the same time, taking the breakthrough on the three-dimensional Ghys conjecture as a starting point, Shanghai AI Laboratory will extend the accumulated reasoning capabilities to other disciplines with homologous mathematical structures; after new breakthroughs are achieved, the new reasoning capabilities will be encapsulated back into the Duanyan platform for reuse, combining with more disciplines to seek the next round of breakthroughs, forming a self-evolving flywheel of "breakthrough—encapsulation—reuse—breakthrough again."

This combination of "human-machine collaboration + formal verification" provides an auditable, reproducible path for AI participation in basic scientific research. As reasoning capabilities migrate to other disciplines, AI for Science may be moving from an auxiliary tool to research infrastructure itself.

AI for Science refers to the systematic application of artificial intelligence methods to natural science discovery, covering directions such as protein structure prediction, materials screening, drug design, mathematical conjecture exploration, and proof verification. Its development has roughly gone through three stages: the early stage focused mainly on data-driven pattern recognition and prediction; the middle stage introduced large-scale pretrained models and generative methods; and the current stage is moving toward a closed-loop research infrastructure form of "agents + formal verification + domain knowledge bases." The proof and verification of the three-dimensional Ghys conjecture is a typical sample of this evolutionary path—AI not only participates in proposing ideas, but also accepts strict auditing through formal systems, giving machine-produced mathematical results reproducible and traceable academic legitimacy.

One-line Summary

Intern-S2 proves the three-dimensional Ghys conjecture through human-machine collaboration; Peking University's SHEAF completes Lean formal verification.

Paragraph Summary

Shanghai AI Laboratory's Intern-S2, through seven batches of successive deduction and human-machine collaboration across 389 nodes, helped Xu Disheng's team tackle the three-dimensional Ghys conjecture, producing a 400-page derivation report in the first round. Peking University's Dong Bin and Liu Ruochuan teams used the independently developed SHEAF framework to complete Lean formal verification of all four main theorems in about 5 days, with peak concurrency of 100 agents and about 550,000 lines of code. Intern-S2 adopts a general-purpose and specialized integration training route and asynchronous long-horizon reasoning reinforcement learning, leading open-source models on benchmarks such as IMO-Proof and surpassing Gemini 3.1 Pro on some metrics. The research forms a new scientific research paradigm of "systematic exploration—expert judgment—accumulation of results—feedback correction," and the capability loop will be encapsulated as modules for the Intern·Duanyan platform, advancing AI from an auxiliary tool toward research infrastructure.