Fundamental groups of special complex varieties and root orbifolds

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Proves Campana’s abelianity conjecture: special compact Kähler manifolds have virtually abelian fundamental groups. Using this theorem, establishes the same conclusion for order-two root orbifolds of smooth projective complex fourfolds along one nonempty smooth connected divisor, when special in the stated differential-line sense. For smooth special complex quasi-projective varieties, proves that every finite-dimensional complex linear representation of the fundamental group has virtually nilpotent image of class at most two.

The release has no Lean statement for this family, so there is no formal statement to compare with the result described above.

What the papers state

Theorem 1.1 (Two-step linear monodromy)

In Two-step monodromy of special quasi-projective varieties, 24 September 2026

The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.

Let V be a connected smooth special complex quasi-projective variety. For every positive integer d and every representation \rho:\pi_1(V)\to\GL_d(\C), the image \rho(\pi_1(V)) has a subgroup of finite index and nilpotency class at most two.

Theorem 1.2 (Completion under quasi-Albanese exactness)

In Two-step monodromy of special quasi-projective varieties, 24 September 2026

Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.

Let V be a connected smooth complex quasi-projective variety and let a:V\to A=\Alb(V) be its algebraic quasi-Albanese map. Suppose a is dominant, choose a smooth connected general fibre F and a point v\in F, and assume that the sequence of ordinary fundamental groups

\pi_1(F,v)\longrightarrow\Gamma:=\pi_1(V,v) \xrightarrow{a_*}\Lambda:=\pi_1(A,a(v))\longrightarrow1

is exact. Then every canonical rational unipotent quotient of \Gamma has nilpotency class at most two. The full rational unipotent completion is a finite-dimensional unipotent algebraic group of class at most two. Every finite-dimensional complex unipotent representation of \Gamma also has image of class at most two.

The release does not say which paper theorem its catalogue describes. Both statements above are shown whole: the paper’s main theorem first, then the statement that shares the most wording with the description. The atlas has not reviewed either choice.

Seven more possible matches

Theorem 1.3 in A conditional abelianity theorem for special fourfold pairs with a half-weight divisor, 5 October 2026.
Theorem 1.1 in The abelianity conjecture for special compact Kähler manifolds, 23 September 2026.
Corollary 1.2 (Fundamental groups in Kodaira dimension zero) in The abelianity conjecture for special compact Kähler manifolds, 23 September 2026.
Corollary 1.5 (Analytically compactifiable covers) in The abelianity conjecture for special compact Kähler manifolds, 23 September 2026.
Corollary 1.3 (Conjecture S and bimeromorphic Iitaka uniformization) in The abelianity conjecture for special compact Kähler manifolds, 23 September 2026.
Theorem 1.3 in Two-step monodromy of special quasi-projective varieties, 24 September 2026.
Corollary 1.4 (Holomorphic convexity for special manifolds) in The abelianity conjecture for special compact Kähler manifolds, 23 September 2026.

Reported proof verification: The release has no Lean statement for this family. The papers are available to read and assess.
Papers and explanations: Three current papers, each readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

The abelianity conjecture for special compact Kähler manifolds

23 September 2026, current edition.

Read it here PDF

We prove that the fundamental group of every special compact Kähler manifold is virtually abelian, resolving Campana’s abelianity conjecture in all dimensions. In particular, every smooth compact connected Kähler manifold of Kodaira dimension zero has virtually abelian ordinary fundamental group.

Two-step monodromy of special quasi-projective varieties

24 September 2026, current edition.

Read it here PDF

We give an independent proof that every complex linear representation of the ordinary fundamental group of a connected smooth special complex quasi-projective variety has virtually nilpotent image of class at most two. This conclusion was previously announced by Cao–Deng–Hacon–Păun. We also construct special open surfaces whose general quasi-Albanese fibres are not special.

A conditional abelianity theorem for special fourfold pairs with a half-weight divisor

5 October 2026, current edition.

Read it here PDF

Using the abelianity theorem for special compact Kähler manifolds in every dimension, we prove virtual abelianity of the entire orbifold fundamental group of the special order-two root orbifold associated with a pair \((X,\tfrac12D)\), where X is a smooth projective fourfold and D is a nonempty smooth connected divisor. We construct a special smooth projective eightfold whose fundamental group surjects onto the required group.

Lean statements

The release has no Lean statement for this family. Its papers remain available to read, and contributors can propose a formal statement of a result. Suggest a change

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

The release contains no Lean statement for this family, so there is no formal statement to compare with OpenAI’s description.

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Within this family

Papers elsewhere in the release that this family’s papers cite

Orbifold and logarithmic Iitaka subadditivityCurrent edition; no accompanying Lean statement Family Iitaka subadditivity, variation, and logarithmic additivityCited by The abelianity conjecture for special compact Kähler manifolds.
A surface counterexample to Shafarevich holomorphic convexityCurrent edition; no accompanying Lean statement Family Shafarevich counterexamples in dimension two and with large fundamental groupCited by The abelianity conjecture for special compact Kähler manifolds.

Papers elsewhere in the release that cite this family’s papers

A surface counterexample to Shafarevich holomorphic convexityCurrent edition; no accompanying Lean statement Family Shafarevich counterexamples in dimension two and with large fundamental groupCites The abelianity conjecture for special compact Kähler manifolds.
Semialgebraic universal covers of normal projective varietiesCurrent edition; no accompanying Lean statement Family Semialgebraic universal covers and bounded domainsCites The abelianity conjecture for special compact Kähler manifolds.

References outside the release

Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanation Suggest a source attribution Suggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Major math journal”. The page says that nothing on it is verified.
Author not stated. Source

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Identify the theorem the catalogue describes

Family 057 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

State the result in Lean

Family 057 The release has no Lean statement for this family. Open the form