31-Year-Old Ghys Conjecture (Codimension-One Case) Proven via Human-AI Collaboration, Verified with 550,000 Lines of Lean Code

Key points

• The problem. In 1995, French mathematician Étienne Ghys asked whether holomorphic Anosov systems on compact complex manifolds can always be brought, via a biholomorphic change of variables, into a clean normal form. The conjecture is considered one of the most important long-standing open problems in dynamical systems; its real-number analogue remains unsolved worldwide.
• The claimed result (October 14 announcement). Professor Xu Disheng's team at Greater Bay Area University, using Shanghai AI Laboratory's InternScience (Shusheng) multimodal large model S2 in a human-AI collaborative workflow, completed a proof of the 3D (codimension-one) Ghys conjecture. Peking University's teams of Professor Dong Bin and Academician Liu Ruochuan performed formal verification with an in-house framework.
• What was actually proven. The paper *Codimension-one holomorphic Anosov diffeomorphisms* proves that every codimension-one holomorphic Anosov diffeomorphism on a compact connected complex manifold is biholomorphically conjugate to a hyperbolic automorphism of a complex torus. This is a slice of the full conjecture (which concerns all compact complex manifolds) — "the staircase, not the whole floor." The paper appeared on arXiv on September 29 and was revised to v3 on October 13 with an AI-usage statement and formalization notes.
• How the human-AI pipeline worked. InternScience S2 ran seven successive derivation batches, expanding the problem graph from 15 to 389 nodes and producing about a thousand pages of rigorous reasoning plus dozens of novel argument strategies. Xu Disheng and his student Zhang Jiesong identified the key breakthrough in the AI's first-round exploration and continuously calibrated direction, forming a closed loop of "systematic exploration, expert judgment, result accumulation, feedback correction." Notably, before the paper's arXiv upload, researcher Xie Junyi at Peking University reportedly failed to find a proof using GPT-6 on the same problem — underscoring that the difference lay partly in the human-machine collaboration, not the model alone.
• Formal verification at scale. Because one error in a long AI-assisted derivation collapses the whole chain, the PKU team's SHEAF framework formalized all four main theorems in about five days of wall-clock time, with peaks of about 100 parallel agents, producing roughly 550,000 lines of Lean code and confirming semantic consistency with the paper's theorems. The team also formalized a batch of foundational results in dynamical systems to address the field's weak formalization infrastructure. PKU previously formalized the Anderson conjecture and, recently, independently completed a formalization of the Poincaré conjecture.
• The pipeline's origin story. In 2025, the Chinese Mathematical Olympiad final introduced an AI test track: InternScience S1 scored 102 points under identical time limits and grading, ranking first among participating models and far above the 78-point gold-medal line. Shanghai AI Laboratory and Xu's team then launched a collaboration in early 2026 to push the model from competition-level to research-level mathematics.
• Three boundaries to keep in mind.
1. The paper is a preprint, not peer-reviewed — final confirmation awaits journal and community scrutiny. 2. The AI's role was assistive: it generated large-scale derivations and candidate strategies, but humans identified the breakthrough and steered direction. Calling this "AI solved the problem" erases the human judgment in the loop. 3. The full conjecture and its real-case analogue remain open. Xu himself described this as only a beginning.
• What's next. The real product may be the reusable pipeline rather than the proof: PKU plans to package the verified capability into a reusable mathematical verification module for the InternScience Endgame (Duanyan) scientific discovery platform. For other problems with "huge search spaces and scarce experts," the transferability of this closed loop is the question to ask.

References

• Jiesong Zhang, *Codimension-one holomorphic Anosov diffeomorphisms*, arXiv:2609.37695[v3], 2026-10-13. https://arxiv.org/abs/2609.37695
• Science and Technology Daily, 2026-10-15: https://www.stdaily.com/web/gdxw/2026-10/15/content_596583.html
• Science Net (Zhao Guangli), 2026-10-15: https://news.sciencenet.cn/htmlnews/2026/10/572932.shtm
• Nanfang Plus, 2026-10-15: https://www.nfnews.com/content/Lownjg9B6J.html
• CGTN, 2026-10-15: https://news.cgtn.com/news/2026-10-15/Chinese-researchers-solve-3D-Ghys-conjecture-with-homegrown-AI-model-1RgD8zQ3Z3a/p.html