Browse › Real and complex analysis › 072 Brennan's conjecture and the integral-means spectrum
Brennan's conjecture and sharp inverse-square integral means
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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$.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Follow-up works
- Ilia Binder, Oleg Ivrii, István Prause, Stanislav Smirnov, Brennan's Conjecture and the Universal Integral Means Spectrum (arXiv:2610.23853 [math.CV], 16 Oct 2026). Cites this paper and its companion and gives a short proof that $B_b(t)\le t^2/4$ for $t\in[-2,2]$. Via Makarov's identity $B(t)=\max\{B_b(t),3t-1\}$, this yields Brennan's conjecture $B(-2)=1$; the authors say they reached it "while validating these results". [family-level]
Comments and discussion
- Ilia Binder, Oleg Ivrii, István Prause, Stanislav Smirnov, §1.2–1.3 of Brennan's Conjecture and the Universal Integral Means Spectrum (arXiv:2610.23853, 16 Oct 2026). The authors write that "none of the techniques appear unprecedented, their combination in this context was missed by the human experts". They add that the AI proofs contain derivations "that, while correct, are redundant". [family-level]
Formalization
- OpenAI math release, Lean scope notes for family 072 (lean/docs/072.md). Describes the release's Lean formalization of the area-integrability range $4/3<s<4$ (equivalently $-2<t<2/3$), the uniform inverse-square bound with exponent $-1-\varepsilon$, $B_{\mathcal S}(-2)=1$, and Koebe divergence at the endpoints. The comparator statements are
Brennan.leanandBrennanSharp.lean. [family-level] - google-deepmind/formal-conjectures, FormalConjectures/Wikipedia/Brennanconjecture.lean (formal-conjectures repository). An independent Lean statement of the unrestricted and bounded Brennan endpoint identities, with proofs left as
sorry; $B(-2)=1$ is taggedresearch solvedwith a link to the OpenAI Lean proof, while $B_b(-2)=1$ remains taggedresearch open. - mo271, feat: mark problems solved in the OpenAI math release and link formal proofs (formal-conjectures PR #6898, merged 11 Oct 2026). This PR marks "Brennan B(-2) = 1" as solved and leaves "Brennan bounded spectrum" open "on purpose".
Related prior literature mentioned by others
- Lars V. Ahlfors, Quasiconformal reflections (Acta Mathematica 109, 1963). Binder et al. identify this as an antecedent of the papers' critical-point maps. [family-level]
Digests and expositions
- AI Proved What?, Four thirds to four? Brennan’s conjecture and the integral-means spectrum (episode 072, October 2026). Animated exposition and transcript covering both claims, Koebe endpoint behavior, the probability-law construction, and the saddle–maximum comparison; its status discussion does not incorporate the Binder–Ivrii–Prause–Smirnov follow-up. [AI-generated per source] [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 072
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:Brennans-conjecture-and-sharp-inverse-square-integral-means-September-24-2026,
author = {{OpenAI}},
title = {{Brennan's conjecture and sharp inverse-square integral means}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/Brennans-conjecture-and-sharp-inverse-square-integral-means-September-24-2026/paper.pdf}{OAI:Brennans-conjecture-and-sharp-inverse-square-integral-means-September-24-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/072.md. The Lean statements have not been checked by people against the paper's claims.
Family 072: Brennan's conjecture and the integral-means spectrum
Proves Brennan's conjecture: for every conformal bijection ϕ from a simply connected plane domain onto the disk, $|\phi'|^s$ is area-integrable for $4/3\lt s\lt 4$. The sharp universal integral-means identity is $B_{\mathcal S}(t)=|t|-1$ for t ≤ −2. A strict bound $B_b(-1)\lt 1/4$ for bounded univalent functions disproves Kraetzer's prediction at that parameter.
Other papers in this family:
- A strict inverse-first-power bound for univalent functions · September 24, 2026