Lean-verified proof said to close the 1995 Ghys conjecture
Shanghai AI Laboratory announced on October 15, 2026 that a research team working closely with the lab's large language model Shusheng-S2 has closed the three-dimensional Ghys conjecture — a problem in complex dynamics that has been open since 1995. What would lift the story above a mere announcement is a formal proof in the Lean proof assistant, where every logical step is machine-verified, and the fact that the formalized code is publicly available. But for now the story rests on the lab's own announcement: no independent confirmation from the mathematics community is documented in the available source material.
What the conjecture is about
The three-dimensional Ghys conjecture was put forward by the French mathematician Étienne Ghys in 1995 and has, according to the coverage, sat at the frontier of complex dynamical systems ever since. The new result, published as preprint 2609.37695 (submitted September 29, 2026, revised October 5, 2026), reportedly settles the codimension-one case: holomorphic Anosov diffeomorphisms on compact complex three-folds (MSN coverage; the link goes to secondary coverage of the preprint, not to arXiv itself).
For non-mathematicians, this translates roughly as follows: Anosov dynamics describes systems in which trajectories with small deviations expand and contract in controlled directions — a form of chaotic but structured motion. Ghys' conjecture concerns when such systems exist in the complex, holomorphic setting, and the three-fold case has been one of the remaining pieces. The details of the proof, and the precise meaning of "codimension one" in this context, cannot be assessed from the available source material — what is reported is the scope: holomorphic Anosov diffeomorphisms on compact complex three-folds.
Who is behind it
The work was organized around Xu Disheng, professor at Great Bay University in Dongguan and visiting scholar at Shanghai AI Laboratory, and Jiesong Zhang, a postdoctoral researcher at KTH Royal Institute of Technology in Stockholm. Zhang earned his doctorate under Xu at Peking University and is the paper's sole author, according to MSN coverage.
One detail worth noting: although the model gets much of the attention, it is a small human team of two that stands behind the actual research work. This is not an example of a model solving a mathematical problem on its own, but of close human–machine collaboration — and that is how the lab itself presents it.
How the working method is described
The work began in August 2026. The approach centered on Shusheng-S2 and the lab's purpose-built "Harness system" — a platform Shanghai AI Lab has developed to support large-scale recursive deduction and high-bandwidth human–machine interaction. That means, to the extent the description can be interpreted, that the model was used to generate and extend chains of reasoning at large scale, while the researchers directed and interpolated in a tight iterative loop.
Here is a source conflict that cannot be resolved from the available material: the MSN coverage calls the model "Shusheng-S2," while the KuCoin rendition of the same announcement uses variants such as "Shuwen-S2" and "Shuying-S2." The most detailed source is the clearest and most consistent in its naming, so this article follows "Shusheng-S2" — but readers should know that the name has not been confirmed against the lab's own primary sources.
The verification chain: what is actually machine-checked
The strongest link in the story is independent of the model claim itself: a team at Peking University, led by Dong Bin and the academician Liu Ruochuan, is said — according to the announcement as reproduced in KuCoin's news flash — to have carried out formal verification of the proof with their own SHEAF framework and found it to be correct. The proof is formalized in Lean, a proof system in which correctness is checked by a machine, step by step, against strict formal rules. The formalized code is publicly available on GitHub, and the preprint is on arXiv.
What does that mean in practice? By this article's own assessment, a Lean verification certifies that the formalized version of the proof follows from the axioms without logical gaps — a guarantee that differs in strength from traditional peer review, which does not machine-check every logical step. But it does not necessarily certify that the formalization captures what the proof claims to prove, and it says nothing about how significant the result is. And crucially: the fact that another team is said to have run the verification is, for now, known only through the lab's own announcement. The code is stated to be publicly available, so it is something third parties could in principle check — but no such third-party check is documented in the sources so far.
The lab's framing — and what is embellishment
Shanghai AI Laboratory emphasizes two points beyond the mathematics itself. The first is that the result, according to the lab, demonstrates the value of a new scientific paradigm — that is, a replicable model for human–AI collaboration in basic research. The second, according to the coverage, is that this is said to be the first time a Chinese large model has contributed to solving a world-class conjecture in pure mathematics.
Both claims should be read as company statements, not established facts. The lab has an obvious interest in presenting its models as scientifically useful, and the "paradigm" language is the grammar of marketing more than of mathematics. The same goes for the "first" claim, which cannot be verified from the available sources. The KuCoin rendition also contains an inexplicable financial intrusion about "CFT and risk-on assets," which is supported nowhere and can safely be ignored.
What remains before this can be taken as fact
The story is, with careless precision: probably big, but unsettled. The most important things to keep track of:
- No independent confirmation. There is no documented validation from the broader mathematics community of either the proof's significance or the Ghys conjecture's actual resolution. Lean verification, if independently checked, could change this quickly — that is the whole point of formalized proofs.
- The primary documents have not been assessed here. The preprint, the GitHub repository and the lab's own announcement are all said to be publicly available, but the coverage this article is based on consists of secondary renditions. Certain details — such as the model name and "Greater Bay Area University" versus "Great Bay University" in the KuCoin version — reveal that the renditions contain careless errors.
- The model's role is unclear. How much of the mathematical work the model contributed, as opposed to the humans, is not described operationally anywhere. "Large-scale recursive deduction" is an architectural label, not an account of what the model actually contributed to the proof.
If the Lean code checks out with independent mathematicians, this outcome will in any case be a milestone worth noting: either as evidence that large models can contribute to serious fundamental mathematics, or as an example of how quickly a "breakthrough" narrative can run ahead of the documentation. For now, only the latter is certain.