If you follow AlphaProof-style AI-for-math, this is the Chinese counterpart story you can actually open and inspect. On roughly October 15, 2026, Shanghai AI Lab said researchers used its science multimodal model Intern-S2 / 书生-S2 to help prove the codimension-one (and therefore 3D) case of the Ghys conjecture — a ~30-year open problem posed by French mathematician Étienne Ghys in 1995. Peking University teams then formally checked the main theorems in Lean. That combination — research-grade conjecture, named Chinese science model, machine-checked Lean — is rare enough that mathematicians and AI engineers abroad can treat the public paper and repo as primary sources, not press-release fog.
The honest framing is assisted, not autonomous. The arXiv paper’s sole author is Jiesong Zhang (张洁松, KTH). His AI-use disclosure states that an internal Intern-S2 helped develop ideas through multiple rounds of dialogue; he independently verified all mathematical arguments and takes full responsibility. The research collaboration also involves Xu Disheng (许地生, Greater Bay University, visiting Shanghai AI Lab), who had long worked on related Ghys questions. AI did not “solve it alone.”
What was proved
Ghys conjectured that every holomorphic Anosov diffeomorphism on a compact complex manifold is biholomorphically conjugate to an affine automorphism of a complex infra-nilmanifold. Zhang’s paper, Codimension-one holomorphic Anosov diffeomorphisms (arXiv:2609.37695), settles the codimension-one case:
- Codimension-one holomorphic Anosov diffeomorphisms on compact connected complex manifolds are biholomorphically conjugate to hyperbolic automorphisms of complex tori.
- That covers complex dimension three in particular (one of the two nonzero invariant distributions must have complex dimension one).
- The higher-dimension general case of Ghys’s conjecture remains open.
How Intern-S2 was used
Shanghai AI Lab’s announcement describes a human–machine loop, not a one-shot solve. Precursor Intern-S1 scored 102 on the 2025 Chinese Mathematical Olympiad AI test (gold line 78). Intern-S2 was then pushed toward research-grade problems. For Ghys, the lab claims:
- 7 reasoning batches of continued derivation
- Problem graph grown from 15 → 389 nodes
- First round about 400 pages; roughly thousands of pages of derivation material overall
Researchers steered which branches to deepen. That is closer to a high-bandwidth research assistant than to an end-to-end theorem prover that ships a finished proof without humans.
Illustration: the second public artifact — Lean formalization of the main theorems, so outsiders can audit the machine-checked chain rather than trust a press quote.
Lean formalization — and one honest asterisk
Peking University teams led by Dong Bin and Liu Ruochuan formalized the main results with their open formalization agent SHEAF. Project claims for that push: about 5 days, peak ~100 agents in parallel, ~550k lines of Lean. The code lives at github.com/frenzymath/HolomorphicAnosov, covering Theorem A and Theorems 1.1, 1.2, 1.3.
Read the repo carefully: some formalized theorems assume HomotopyTorusRigidity — the Hsiang–Wall 1969 torus case of the Borel conjecture — rather than re-proving that classical topological ingredient from scratch inside Lean. That is normal for research formalization (import a known theorem as an axiom or hypothesis), but it means “Lean-checked” here is not “every dependency in the mathematical universe was rebuilt in this repo.”
You can read the paper on arXiv, clone the Lean repo, and compare the workflow to AlphaProof-style formalization stories. You cannot download Intern-S2 weights from a public Hugging Face card for this announcement — the story’s public deliverables are the math and the Lean, not a general-purpose science model checkpoint you fine-tune at home.
What this changes for people outside China
For mathematicians in complex dynamics, the paper is the product: a classification result that had been open since 1995 in the codimension-one setting, with an explicit remaining gap in higher dimension. For AI researchers and formal-methods engineers, the interesting package is the combination of (1) a disclosed internal science LLM used for idea exploration, (2) a named human author who owns the proof, and (3) a large Lean formalization produced with multi-agent tooling on a research theorem — not a contest problem. That is a different maturity signal than “model scored X on a benchmark.”
If you are trying to decide whether Chinese AI-for-math is worth tracking alongside DeepMind-style efforts, this is a concrete datapoint: the artifacts you can open today are arXiv:2609.37695 and HolomorphicAnosov. Start there. Treat lab claims about page counts and agent peaks as process color; treat the theorem statement and the Lean assumptions as the load-bearing claims.