Shanghai AI Laboratory says its scientific multimodal model Intern-S2 helped mathematicians prove the three-dimensional case of the Ghys conjecture, a problem in complex dynamics posed in 1995 by the French mathematician Etienne Ghys. A team at Peking University then checked the main results with the Lean theorem prover.
The paper, Codimension-one holomorphic Anosov diffeomorphisms, was posted to arXiv on September 29 and revised on October 13. It lists a single author, Jiesong Zhang of KTH Royal Institute of Technology. It proves that every codimension-one holomorphic Anosov diffeomorphism of a compact connected complex manifold is biholomorphically conjugate to a hyperbolic automorphism of a complex torus, which settles the conjecture in that case and in complex dimension three. Roughly, the conjecture says that if a space supports this kind of chaotic but perfectly regular motion, the space itself must have a rigid, crystal-like structure.
The lab's announcement credits the work to a team led by Disheng Xu, a professor at Great Bay University and visiting scholar at the lab, with Zhang, his former student, joining as a visiting scholar. In a declaration of AI use, Zhang writes that he used an internal version of Intern-S2 to help develop the ideas and arguments through multiple rounds of dialogue, and that he independently verified all of the mathematics. He thanks Xu for continued discussions on the problem.
According to the lab, the model produced a 400-page derivation report in its first round of reasoning. Over seven further rounds, its problem graph grew from 15 nodes to 389 and its output reached about a thousand pages, while the mathematicians identified the key openings, corrected its direction and assembled the final proof.
The paper's four main theorems, together with the results of Ghys that it relies on, were formalized by the team of Bin Dong and Ruochuan Liu at Peking University using SHEAF, an open-source formalization agent the team built. Team members Jiedong Jiang and Bin Wu said the work took about five days, with up to 100 agents running in parallel, and produced about 550,000 lines of Lean code. Experts checked that the formal statements match the theorems in the paper. The code is public on GitHub.
Shanghai AI Laboratory says it will package the workflow as a reusable mathematical verification module for its scientific discovery platform.
SEE ALSO: Shanghai AI Lab Ships Intern-S2-397B Science Multimodal Model