Brennan's conjecture and sharp inverse-square integral means

Lean formalization in OpenAI math repository (Result 072)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Brennan's conjecture and sharp inverse-square integral means'. We prove Brennan's conjecture: if a simply connected plane domain admits a conformal bijection φ onto the unit disk, then |\varphi'|^s is area-integrable for every 4/3\lt s\lt 4. We also prove the sharp inverse-square integral-means exponent B_{\mathcal S}(-2)=1 for the normalized schlicht class \mathcal S.

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

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository