Lean formalization in OpenAI math repository (Result 027)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Integral points on character varieties of curves'. We prove potential Zariski density of integral points on SLr-character varieties of smooth complex curves in every rank. The result allows prescribed quasi-unipotent boundary monodromy, including exact nonsemisimple conjugacy classes, and holds on every component over the full ring of integers of one finite extension. Here integrality is measured in the ambient character variety, while the exact boundary conditions are imposed on the complex representation.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 027). The Lean development was not rebuilt locally.