View source for 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 ([https://github.com/openai/math 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'''<sup>''n''</sup> 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); [https://arxiv.org/abs/1104.2309v2 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'''<sup>''m''</sup> × ''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 <code>1581d4c</code> of the openai/math repository:
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Semialgebraic-universal-covers-of-normal-projective-varieties-September-24-2026 ''Semialgebraic universal covers of normal projective varieties''];
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Symmetry-of-semialgebraic-bounded-domains-with-compact-quotient-September-24-2026 ''Symmetry of semialgebraic bounded domains with compact quotient''].
* '''Formalization, as described by the repository.'''
** The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/058.md 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/SymmetricDomains.lean SymmetricDomains.lean] states <code>main</code>. Its hypotheses are:
*** ''U'' is a connected, bounded, semialgebraic subset of an affine algebraic set in '''C'''<sup>''n''</sup>, 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 ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 17 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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'''<sup>''m''</sup> × ''F'', the quasi-projective criterion and the corollary for varieties covered by '''C'''<sup>''n''</sup> are not stated. Records a sandboxed Comparator pass for <code>SymmetricDomains</code>. || 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, fuel, memory, errors) does not list <code>SymmetricDomains</code>. The challenge was therefore accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-10 || [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/SymmetricDomains.json cert-machine], openai/math lane K, run 38019899278 || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>SymmetricDomains</code> 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 <code>main</code> 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.

[[Category:OpenAI results]]