News · 2026-10-19

Intern-S2 assisted a proof of a restricted Ghys-conjecture case, with Lean checks

Jiesong Zhang has proved the codimension-one case of Ghys’s conjecture, including the complex-dimension-three case, and disclosed help from an internal Intern-S2 model. The paper’s central results were separately formalized in Lean with human verification. Shanghai AI Lab’s October 15 account describes an iterative collaboration, rather than an autonomous model solving the full conjecture.

Key facts

• The result covers the codimension-one case, which includes complex dimension three.
• The theorem appeared in the September 29 first version; AI-use disclosures were added in the October 13 third version.
• Zhang is the sole paper author; the formalization work involved a separate Peking University team.
• Primary sources are the paper and version history and Shanghai AI Lab’s account.

The news is both a mathematical result and a more detailed record of how AI participated in producing it. Viral descriptions often compress those into a sentence saying a model solved a conjecture. Here the public record supports a more informative division of labor: model-assisted exploration, human selection and responsibility, followed by formal checking of central statements.

Zhang titled the paper “Codimension-one holomorphic Anosov diffeomorphisms.” In ordinary language, it concerns highly structured dynamical systems that expand in some directions while contracting in others, with additional constraints from complex geometry. The conjecture asks whether such systems must ultimately correspond to a particular class of familiar geometric models.

A rough analogy is discovering that an intricate-looking mechanism is a standard gearbox viewed through a complicated coordinate system. The theorem identifies when the apparent complexity can be transformed into a simpler, well-understood form. In the case proved here, the system becomes a hyperbolic automorphism of a complex torus under the appropriate change of coordinates.

The scope matters. A result for a restricted case can be a real advance without resolving every case of a general conjecture. Complex dimension three is especially relevant because geometric complications appear beyond the surface setting. Readers should not translate that dimensional statement into a claim that the full conjecture is now closed.

The current full text describes the proof strategy. It constructs a way of linearizing stable leaves so certain geometric motions become globally defined, avoiding an earlier transitivity assumption. An estimate on antiholomorphic derivatives then helps establish the needed holomorphic structure. Together, the steps produce the torus classification. The result is a geometric argument, rather than a report that a computer searched every possible system.

Zhang’s declaration says he used an internal version of Intern-S2 over multiple dialogue rounds to develop ideas and arguments, independently checked the mathematics and takes responsibility for the manuscript. Shanghai AI Lab describes researchers choosing promising directions and redirecting unsuccessful ones. Disheng Xu participated in that collaboration and is acknowledged in the paper, whose sole listed author remains Zhang.

The lab’s account includes extensive generated derivations. Output volume is useful context for the search process, but pages produced do not measure mathematical validity or the amount of human work saved. The stronger evidence is the final argument and its checks. The reviewed material does not present the internal model as a downloadable checkpoint with a public deployment specification.

The formalization declaration adds another layer. It credits a Peking University team associated with Bin Dong and Ruochuan Liu, using SHEAF, and names Jiedong Jiang and Bin Wu for formalization and human verification of the final theorem. Lean checks the encoded mathematical claims against its proof rules. That is stronger than asking another language model whether a proof looks persuasive.

It still leaves a translation boundary. The formal statement must express the intended informal theorem, and supporting assumptions must be appropriate. Autoformalization and proof assistants explain why a machine check is powerful without making every surrounding scientific judgment automatic. The disclosures do not claim the entire manuscript has completed independent external peer review.

The first version also clarifies the timeline: the theorem predates the later AI and formalization disclosures. October’s news is not a brand-new first posting of the theorem. It is a clearer account of the collaboration and its verification, made visible through the revised paper and lab announcement.

In the Reddit discussion, readers challenged the autonomous-solution framing. That correction matches the primary record; anecdotal claims about the model’s performance on unrelated problems do not evaluate this proof. The significant conclusion is a specific theorem with disclosed AI assistance and formal checks, accompanied by an unusually useful reminder that scientific credit and responsibility remain more detailed than a model headline.

Primary source, verified: read the paper → (arXiv 2609.37695)

Ground Truth. (2026, October 19). Intern-S2 assisted a proof of a restricted Ghys-conjecture case, with Lean checks. Ground Truth. https://groundtruth.day/news/intern-s2-assisted-proof-covers-codimension-one-ghys-case.html

@misc{groundtruth:intern-s2-assisted-proof-covers-codimension-one-ghys-case,
  title  = {Intern-S2 assisted a proof of a restricted Ghys-conjecture case, with Lean checks},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {oct},
  url    = {https://groundtruth.day/news/intern-s2-assisted-proof-covers-codimension-one-ghys-case.html}
}

Topics: mathematics · science · formal-verification · ai-assisted-research