AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

A strict inverse-first-power bound for univalent functions

Can the mathematical statement in A strict inverse-first-power bound for univalent functions 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 072)

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 'A strict inverse-first-power bound for univalent functions'. We prove a uniform upper bound for inverse-first-power integral means of normalized univalent disk maps with exponent strictly below 1/4. Consequently, the bounded universal integral-means spectrum satisfies B_b(-1)\lt 1/4, disproving Kraetzer's conjectured spectrum at p = −1.

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