AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Symmetry of semialgebraic bounded domains with compact quotient

Can the mathematical statement in Symmetry of semialgebraic bounded domains with compact quotient be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 058)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Symmetry of semialgebraic bounded domains with compact quotient'. Every nonempty connected semialgebraic bounded open subset of a complex affine variety admitting a properly discontinuous cocompact group of biholomorphisms is smooth and biholomorphic to a bounded symmetric domain. This answers the bounded-domain question of Kollár and Pardon affirmatively.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 058). The Lean development was not rebuilt locally.