Brennan's conjecture
From OpenAI Aftermath
Brennan's conjecture asks whether, for every conformal bijection φ from a simply connected plane domain onto the unit disk, the function |φ′|s is area-integrable for 4/3 < s < 4. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), both dated 24 September 2026, claim a proof of the conjecture and a strict bound that disproves Kraetzer's conjectured integral-means spectrum at the exponent −1. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the manuscripts:
- Brennan posed the problem in 1978. For the inverse map f = φ−1 from the disk, a change of variables turns the area integral into the integral of |f′|2−s over the disk, so the conjectured range becomes −2 < t < 2/3, and the endpoint question concerns the integral-means spectrum B(t) of univalent maps at t = −2.
- Carleson and Makarov related negative integral means to the distribution of harmonic measure and proved that the spectrum equals |t| − 1 for all sufficiently negative t. Bertilsson reported the area range 4/3 < s < 3.421. The weighted Bergman-space methods of Hedenmalm and Shimorin gave the bound 1.218 for the spectrum at t = −2, and Sola reported 1.206.
- From experiments with conformal maps onto bounded domains, Kraetzer predicted that the bounded universal spectrum is Bb(p) = p2/4 for |p| ≤ 2 and |p| − 1 for |p| ≥ 2. Before the manuscripts, the published upper bounds at p = −1 were 0.403 (Hedenmalm and Shimorin) and 0.388 (Sola).
The original results
- Brennan's conjecture. Theorem 1.1 of Brennan's conjecture and sharp inverse-square integral means states that for every ε > 0 there is a constant Cε such that the circular mean of |f′|−2 on the circle of radius r is at most Cε(1 − r)−1−ε for every normalized univalent map f of the disk and every 1/2 ≤ r < 1, and that the spectrum of the normalized univalent class at −2 equals 1. It states that every conformal bijection φ from a simply connected domain whose boundary in the Riemann sphere has at least two points onto the disk satisfies Brennan's integrability for 4/3 < s < 4. The manuscript also derives the value |t| − 1 of the spectrum for every t ≤ −2, and shows with the Koebe function that both endpoints of the range fail.
- Method, as described: hypothetical excess growth is encoded in a probability law on a compact class of normalized univalent maps of the upper half-plane, built from a positive operator that averages changes of base point. The law forces a sign on an expected Jacobian, and a pairing of critical points of a family of target potentials forces the opposite sign.
- Kraetzer's prediction. Theorem 1.1 of A strict inverse-first-power bound for univalent functions states that there are constants 0 < ε < 1/4 and C such that the circular mean of |f′|−1 is at most C(1 − r)−1/4+ε for every normalized univalent map f and every 1/2 ≤ r < 1, so that Bb(−1) < 1/4 and Kraetzer's conjectured identity is false. The manuscript states that the gap is not evaluated numerically and that the value at p = 1 is not settled.
- Sources. The manuscripts at commit
1581d4cof the openai/math repository:- Brennan's conjecture and sharp inverse-square integral means (24 September 2026);
- A strict inverse-first-power bound for univalent functions (24 September 2026).
- Formalization, as described by the repository. The scope note lean/docs/072.md states that the Lean formalization establishes Brennan's interval, area integrability of |f′|t for univalent disk maps when −2 < t < 2/3, the uniform inverse-square bound with exponent −1 − ε, the spectrum value 1 at −2, divergence at all four boundary exponents for the Koebe map and its inverse, and the strict bound Bb(−1) < 1/4. It lists three Comparator statements:
Brennan.lean,BrennanSharp.leanandStrictMeans.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 19 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math at commit adc7f12, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | t| − 1 is stated only at t = −2, not for all t ≤ −2. | The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet. |
| 2026-10-11 | Formal Conjectures pull request #6898 (Brennanconjecture.lean at commit 3dfd999) |
Statement; formal link | Marks part 1 of the repository's statement of Brennan's conjecture, the value 1 of the universal spectrum of normalized univalent maps at −2, as solved and links the collection's Lean theorem as the formal proof. Part 2, the same value for the spectrum of bounded maps, remains tagged open in that file. | Merged; the file had no later change when checked. |
| 2026-10-16 | I. Binder, O. Ivrii, I. Prause, S. Smirnov, Brennan's Conjecture and the Universal Integral Means Spectrum (arXiv:2610.23853, v1) | Reading (validation) and extension |
The authors state that while validating the two manuscripts they found much of the argument redundant and arrived at a drastically shorter proof of a significantly stronger statement.
|
arXiv preprint (version 1 only). |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
