The Kollár–Pardon conjecture on semialgebraic universal covers

The Kollár–Pardon conjecture predicts which universal covers of projective varieties admit a finite real-algebraic description. Up to biholomorphism, such a universal cover should be a product of a bounded symmetric domain, a complex affine space and a simply connected projective variety. Here a finite real-algebraic description means being a semialgebraic open subset of a projective variety. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), both dated 24 September 2026, make claims on this problem. The first claims the conjecture for connected normal projective varieties. The second claims an affirmative answer to a related bounded-domain question that Kollár and Pardon posed in the same paper. This page summarizes the published claims and lists publicly available follow-up work.

Background

Definitions, as in the manuscripts. A subset of a complex algebraic variety is semialgebraic if, in affine charts, it is a finite Boolean combination of real polynomial equalities and inequalities in the real and imaginary coordinates. A bounded symmetric domain is a connected bounded domain in which every point is an isolated fixed point of a holomorphic involution.
As recounted in the classification manuscript:
- Iitaka's uniformization problem asks whether a smooth projective variety covered by Cⁿ is a finite unramified quotient of an abelian variety. Nakayama proved the relevant structure theorem assuming semiampleness of the canonical divisor.
- Claudon, Höring and Kollár classified quasi-projective universal covers assuming the abundance conjecture.
- Semialgebraic openness allows an additional bounded symmetric factor. Kollár and Pardon formulated the product conjecture as Conjecture 2 of Algebraic varieties with semialgebraic universal cover (Journal of Topology 5 (2012); arXiv:1104.2309v2). They proved a case in which a quotient of the fundamental group acts freely, properly discontinuously and cocompactly on an irreducible bounded symmetric domain of dimension at least two.
As recounted in the bounded-domain manuscript:
- Kollár and Pardon posed the bounded semialgebraic domain question as Question 25 of the same paper (arXiv version 2). The manuscript describes it as distinct from the universal-cover classification.
- Related rigidity results include Wong's characterization of the ball and Rosay's localization, and Frankel's theorem that a convex hyperbolic domain with compact quotient is biholomorphic to a bounded symmetric domain.

The original results

The classification (24 September 2026). Theorem 1.1: let X be a connected normal projective complex variety with universal cover X̃. Then X̃ is biholomorphic to a semialgebraic open subset of a projective variety if and only if X̃ ≃ D × C^m × F. Here D is a bounded symmetric domain and F is a simply connected normal projective variety; either may be a point. No algebraicity of the deck transformations is assumed.
- The collection's summary adds that the universal cover is quasi-projective exactly when the bounded symmetric factor is absent.
- Inputs from the collection. The manuscript states that its group-theoretic input is another manuscript of the collection, The abelianity conjecture for special compact Kähler manifolds: the fundamental group of a smooth special compact Kähler manifold is virtually abelian. It also uses the zero-boundary case of the collection's Log abundance in characteristic zero for the premise of Claudon, Höring and Kollár.
The bounded-domain question (24 September 2026). Theorem 1.1: let U be a nonempty connected semialgebraic bounded open subset of a complex affine variety, on which a group of biholomorphisms acts properly discontinuously with compact quotient. Then U is smooth and biholomorphic to a bounded symmetric domain.
- Finite stabilizers are allowed, the ambient variety may be singular, and no smoothness or projectivity is assumed for the quotient.
- Method, as described: the first step extends Rosay's localization by holomorphic peak functions to open subsets of possibly singular affine varieties. The later sections treat noncollapse, scaling and symmetry.
- The manuscript states that this proof is independent of the classification.
Sources. Commit 1581d4c of the openai/math repository:
- Semialgebraic universal covers of normal projective varieties;
- Symmetry of semialgebraic bounded domains with compact quotient.
Formalization, as described by the repository.
- The scope note lean/docs/058.md links only the bounded-domain manuscript. It states that the formalized result answers that manuscript's symmetry question affirmatively, with the action not necessarily free and the ambient algebraic set possibly singular.
- The Comparator challenge SymmetricDomains.lean states main. Its hypotheses are:
  - U is a connected, bounded, semialgebraic subset of an affine algebraic set in Cⁿ, relatively open in it;
  - a discrete group acts properly on U by holomorphic maps, with compact orbit space.
- Its conclusion: U is smooth and biholomorphic to a bounded symmetric domain, defined as above.
- The classification theorem is not among the selected statements.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 17 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit `c76f1e4`, 14 October 2026)	Review (fidelity of the formal statements)	Rates the family "supporting-only": only the bounded-domain symmetry statement is formalized. The classification of semialgebraic universal covers as D × C^m × F, the quasi-projective criterion and the corollary for varieties covered by Cⁿ are not stated. Records a sandboxed Comparator pass for `SymmetricDomains`.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit `fd4aeeb`, the journal's table of exceptions (time-outs, fuel, memory, errors) does not list `SymmetricDomains`. The challenge was therefore accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-10	cert-machine, openai/math lane K, run 38019899278	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the `SymmetricDomains` solution (1,457 s). The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.

Notes

The kernel checks above concern the formal statement main of the bounded-domain manuscript as written. The classification theorem has no formal statement in the collection.
The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.