Codimension-one holomorphic Anosov diffeomorphisms
Ghys conjectured in 1995 that every holomorphic Anosov diffeomorphism of a compact complex manifold is holomorphically conjugate to an automorphism of a complex infra-nilmanifold, and proved it for complex surfaces. Does the conjecture hold in complex codimension one, that is when or ? This case contains every compact complex threefold.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-assisted
- Method
- —
- Field
- Holomorphic dynamical systems
- Posed by
- Étienne Ghys, Holomorphic Anosov systems, Invent. Math. 119 (1995), 585-614 (conjecture on p. 586)
- Year posed
- 1995
- Years open
- 31y
- Solved
- 2026-09-29
- Model
- Intern-S2 (internal version)
- Vendor
- Shanghai AI Lab
- Collaborators
- Jiesong Zhang
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 24 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Jiesong Zhang 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. This settles Ghys's conjecture in that case, and so for all compact complex threefolds, where Xu and Zhang (2024) recorded it as open.
The proof removes the topological transitivity assumption from Ghys's Theorem B to get a topological conjugacy to a hyperbolic toral automorphism, proves that both invariant distributions are holomorphic (the stable one by an estimate), and shows a torus with holomorphic invariant distributions carries the standard complex structure. Cantat (2004) had the codimension-one case for projective manifolds.
The paper also gives a nilmanifold example whose invariant distributions are smooth but not holomorphic, so the method stops at codimension one. The general conjecture remains open.
What the AI did
The paper's Declaration of AI Use says the author used an internal version of Intern-S2 (Shanghai AI Lab) through multiple rounds of dialogue to assist in developing the mathematical ideas and arguments. It does not say which lemmas or constructions came from the model. The author states that he independently verified all arguments and takes full responsibility.
Separately, Theorem A and Theorems 1.1 to 1.3, with the parts of Ghys's 1995 paper they rely on, were formalised in Lean by the Bin Dong and Ruochuan Liu team at Peking University with their formalisation agent SHEAF; Jiedong Jiang and Bin Wu did the formalisation and the human check of the final statements (paper v3, 13 October 2026).
Verification
No independent mathematician has checked this yet. Read by this site on 15 October 2026, not rebuilt. Repository frenzymath/HolomorphicAnosov, commit 65f2b33 (Lean 4.35.0-rc1, Mathlib, about 4,230 files and 528,000 lines). With comments stripped, the library and Comparator/Solution.lean contain no sorry, admit, axiom declarations, opaque, unsafe, implemented_by, extern or native_decide; several comments still say 'Stage 2 sorry' and are stale. The four headline statements in Comparator/Challenge.lean were read: compact connected complex manifold, biholomorphic f, a smooth metric with an invariant continuous splitting and an iterate contracting each bundle, one bundle of complex rank one; conclusion a biholomorphism to conjugating f to a hyperbolic complex-linear lattice automorphism. Theorems A, 1.1 and 1.3 take as a hypothesis HomotopyTorusRigidity (closed smooth homotopy n-tori, n at least 5, are homeomorphic to the torus), a 1969 theorem of Hsiang and Wall that is not in Mathlib; the definition read here is a true statement, so the hypothesis is not vacuous. The Comparator acceptance and the axiom list are the authors' own; there is no CI and nothing was run here. No independent formalisation anchors the statement (none found in Formal Conjectures), so Lean-checked, not Lean-verified.
Sources
Submitted by FrostyBadger576 on