Shanghai AI Lab says Intern-S2 helped prove the 3D Ghys conjecture; PKU team formalized it in Lean
Shanghai AI Lab announced a 3D Ghys conjecture proof on Oct 15. The paper credits Intern-S2 with helping develop ideas; PKU formalized its theorems in Lean.
The 3D Ghys conjecture concerns holomorphic Anosov diffeomorphisms on complex manifolds. On October 15, Shanghai AI Laboratory (Shanghai AI Lab) announced that a research team had proved it. The v3 arXiv page lists Jiesong Zhang as the sole author; Zhang’s AI-use statement says he used an internal version of Intern-S2, through multiple rounds of dialogue, to help develop the paper’s mathematical ideas and arguments. The same statement says he independently verified all mathematical arguments and takes full responsibility for the manuscript. A Peking University team separately formalized the relevant theorems in Lean, with code published on GitHub.
Key points
- The paper’s theorem concerns a codimension-one holomorphic Anosov diffeomorphism on a compact, connected complex manifold; it says the map is biholomorphically conjugate to a hyperbolic automorphism of a complex torus.
- Shanghai AI Lab says the exploration graph grew from 15 to 389 problem nodes, began with a roughly 400-page report and went through seven rounds of reasoning.
- Shanghai AI Lab and TMTPost report that the PKU team spent about five days on formalization, with a peak of 100 parallel agents, producing roughly 550,000 lines of Lean code.
The 3D Ghys conjecture
Ghys proposed the conjecture in 1995. “Three-dimensional” refers to the complex-geometry problem in the paper, whose theorem also requires a compact, connected manifold and a holomorphic map of codimension one. Shanghai AI Lab calls it a world-level open math problem solved with help from its S2 model. The v3 arXiv AI-use statement is narrower and identifies one author: Jiesong Zhang says he used an internal Intern-S2 to help develop the paper’s mathematical ideas and arguments, independently verified all mathematical arguments and takes responsibility for the manuscript.
This story brings together three kinds of material: the arXiv v3 author statement describes Intern-S2’s role; Shanghai AI Lab’s announcement reports the exploration process; and the GitHub repository lists the Lean formalization targets and their assumptions. Project-reported process metrics do not replace the mathematical argument, and code size does not measure the model’s contribution. For other AI-math coverage, see our entries on AlphaProof Nexus and OpenAI’s AI math manuscripts; those are separate events, not evidence for this result.
How the proof developed
Shanghai AI Lab says the collaboration began in early 2026 and that exploration of the conjecture from multiple angles started in August. TMTPost separately reports that Xu Disheng became a visiting scholar at the lab in March and that Intern-S2 and its supporting system had matured through internal iteration by August. The official announcement says an initial report ran to about 400 pages and was followed by seven reasoning rounds; the problem graph expanded from 15 to 389 nodes, with thousands of pages of derivations and multiple proof approaches. Researchers assessed directions and gave feedback while the model handled large-scale exploration. These dates and process figures are project-reported details, not independent evidence that the mathematical result is correct.
The v3 arXiv AI-use statement is in the singular: sole author Jiesong Zhang says he used an internal Intern-S2 through multiple rounds of dialogue to help develop the paper’s mathematical ideas and arguments. The statement also says Zhang independently verified all mathematical arguments and takes full responsibility for the manuscript. It does not attribute particular lemmas line by line, so the statement alone cannot assign the full proof contribution to the model.
What Lean checked
Formalization supplies a second route for examining the result. The PKU team led by Dong Bin and Liu Ruochuan used SHEAF to represent theorems and dependencies as Lean statements, then coordinated parallel agents to fill in proofs. The code is public in frenzymath/HolomorphicAnosov. Its README says the project formalizes Theorem A and Theorems 1.1, 1.2 and 1.3, with no sorry in those proofs, and that the Lean comparator accepts the solution. Shanghai AI Lab and TMTPost describe the codebase as roughly 550,000 lines of Lean. The repository README gives no exact line count, so this article does not state one.
One assumption deserves a precise explanation. Theorems A, 1.1 and 1.3 take HomotopyTorusRigidity as a hypothesis. The README identifies it as the torus case of the Borel conjecture and notes that Hsiang and Wall proved it in 1969. This is a classical mathematical input in the stated results, not a missing proof or an unfinished formalization. Theorem 1.2 does not use it. When checking the code, readers should look at both which theorems are proved and which established results they assume.
| Item | What the public materials say |
|---|---|
| Paper’s result | A codimension-one holomorphic Anosov diffeomorphism is biholomorphically conjugate to a hyperbolic automorphism of a complex torus |
| Model’s role | Sole author Jiesong Zhang says an internal Intern-S2 helped develop proof ideas through multiple rounds of dialogue |
| Formalized targets | Theorem A and Theorems 1.1, 1.2 and 1.3 |
| Project scale | About five days, peak concurrency of 100 agents; project sources report roughly 550,000 Lean lines |
| Stated premise | Theorems A, 1.1 and 1.3 use HomotopyTorusRigidity; Theorem 1.2 does not |
How to check it
For a quick first pass, open the paper abstract and the formalization repository’s README. The paper states the mathematical claim and its AI-use disclosure; the README lists the formalized results, Lean version and explicit premise. To try the build locally, the repository documents fetching the Mathlib cache and building the project:
lake exe cache get
lake build
The README also gives a comparator command for checking the solution against locked theorem statements. The project specifies leanprover/lean4:v4.35.0-rc1; a machine without the required toolchain and dependencies may need setup before those commands work.
The public repository lets readers inspect the formalization targets and code. The arXiv page lists the paper as a preprint; the sources reviewed here do not provide a peer-review outcome or a verdict on acceptance by the mathematical community, so this article does not claim either. A build without sorry also does not mean every prerequisite has been reproved in this repository: HomotopyTorusRigidity makes that boundary explicit.
Our take
The useful part of this story is the public boundary between two questions: what did the model contribute to the research process, and how can the resulting mathematical claims be checked? The paper’s disclosure addresses the first only at a high level. The Lean repository gives a more concrete artifact for the second: readers can inspect the theorem statements, dependencies and formal proof, including its assumptions. Separate teams and tools handled exploration and formal verification.
For researchers and AI-tool builders, the useful question is how model-assisted mathematical exploration connects to formal verification. Lean checks the definitions and proofs as encoded; it does not automatically establish that those definitions capture the intended mathematical claim. The arXiv page lists a preprint, and the sources reviewed here give no peer-review outcome or verdict on acceptance by the mathematical community.