# Semialgebraic universal covers and bounded domains

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Symmetry of semialgebraic bounded domains with compact quotient](../../preprints/Symmetry-of-semialgebraic-bounded-domains-with-compact-quotient-September-24-2026/paper.pdf)

## Scope

The formalized result answers the paper's symmetry question affirmatively. A nonempty connected bounded semialgebraic subset, relatively open in a complex affine algebraic set, is smooth and biholomorphic to a bounded symmetric domain whenever a discrete group acts properly and holomorphically with compact quotient.

The action need not be free, and the ambient algebraic set may be singular.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Symmetry of semialgebraic bounded domains | [SymmetricDomains.lean](../ComparatorChallenges/SymmetricDomains.lean) |