Brennan’s conjecture: experts confirm and shorten OpenAI’s proof
Result confirmed
Importance: historic (5 of 5)The takeaway
The first famous result from OpenAI’s October maths release to be checked by leading experts in its field: four complex analysts, including Fields medallist Stanislav Smirnov, found no gap. They say the AI combined known techniques in a way ‘missed by the human experts’.
Status
- Claim
Result confirmed
- Our reporting
- High confidence
- Verification
- Lean-verified
- Importance
- Historic (5 of 5)
- Last verified
- 19 October 2026
Your AI and this story
- GPT-6 Astra169 days after its cutoff
- Claude Opus 5.5108 days after its cutoff
- Gemini 4 Argon199 days after its cutoff
- Grok 4.7138 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 108 days before it.
Key facts
- Paper: Binder, Ivrii, Prause, Smirnov, ‘Brennan’s Conjecture and the Universal Integral Means Spectrum’, arXiv 2610.23853 [math.CV], submitted 16 Oct 2026, announced 19 Oct
- Brennan’s conjecture (1978): for every conformal map g from a simply connected proper plane domain onto the disc, ∫|g′|^p dA < ∞ for 4/3 < p < 4; equivalent to B(−2) = 1 for the universal integral-means spectrum (Carleson–Makarov reduction)
- OpenAI’s claim: family 072 of github.com/openai/math, ‘Brennan’s conjecture and sharp inverse-square integral means’ and ‘A strict inverse-first-power bound for univalent functions’ (both dated 24 Sept 2026). They prove Brennan and B_b(−1) < 1/4, which contradicts Kraetzer’s prediction B_b(t) = t²/4. OpenAI’s Lean scope note says the formalization covers the Brennan interval, B_S(−2) = 1 and B_b(−1) < 1/4
- New theorem (human-written): B_b(t) ≤ t²/4 for t ∈ [−2, 2], strict on ]−2, 2[ \ {0}; by Makarov’s identity also B(t) < t²/4 on ]−2, 6 − 4√2[ \ {0}. This strengthens OpenAI’s single-point disproof at t = −1 to the whole interval
- On the AI proof: ‘Two OpenAI preprints released in October 2026 presented a dramatic advance.’ The AI proofs ‘contain a significant number of derivations that, while correct, are redundant and do not seem to contribute either to strength or clarity of the results’
- AI disclosure: ‘When the OpenAI proofs appeared, at first we were puzzled by a seemingly mysterious chain of thought. However, within a day we independently realized that many of the arguments were redundant… Only some of us used AI agents to help with understanding, and the write up below was done without AI help’
- Tone: ‘this was a pleasant and fruitful AI-human interaction in mathematics: there was a spectacular progress, human community was brought together, new results are about to follow, and no robots or humans were harmed.’ The abstract ends with Rick Blaine’s line from Casablanca: ‘AI, we hope this is the beginning of a beautiful friendship’
- Next: the authors say further progress ‘would be computationally intensive, and we have tried to use AI tools to this effect. The results will be reported in a separate preprint’
Show 1 more
- Context: Wikipedia’s Brennan conjecture article (checked 19 Oct) lists OpenAI’s September preprint as an unverified claim. No Hacker News thread and no high-reach X post about the new paper found on the morning of 19 Oct
What happened
Brennan’s conjecture (James Brennan, 1978) concerns how wildly a conformal map can distort area near the boundary: for a conformal map g of a simply connected domain onto the unit disc, |g′|^p should be area-integrable for every 4/3 < p < 4. Carleson and Makarov reduced it, with many other questions in geometric function theory, to the universal integral-means spectrum B(t), and Brennan’s conjecture becomes B(−2) = 1. Kraetzer had conjectured more generally that B_b(t) = t²/4 for |t| ≤ 2. The authors note that evidence against that formula had recently been building up.
OpenAI’s 6 Oct release of 722 AI-written manuscripts (see OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems) included family 072, two papers dated 24 Sept that claim Brennan’s conjecture and a strict bound B_b(−1) < 1/4, which refutes Kraetzer at t = −1. OpenAI lists a Lean formalization for both.
Ten days later Binder (Toronto), Ivrii (Tel Aviv), Prause (Åbo Akademi, Turku) and Smirnov (Geneva), all long-time workers on this spectrum, posted their response. They describe the AI argument (superharmonic potentials, a critical-point map whose Jacobian sign separates maxima from saddles, a weighted signed-area inequality, and a probabilistic averaging step for the strict bound) and trace each ingredient to earlier literature. Then they give a short proof of a stronger theorem, written without AI.
Why it matters
This is the first famous claim in OpenAI’s release that the leading specialists have publicly checked, and the verdict is positive. It also gives a concrete expert assessment of what the AI did: correct but bloated proofs, with no new techniques, combined in a way the field had missed. Their wording (“puzzled by a seemingly mysterious chain of thought”, “within a day”) shows how human understanding can catch up with an AI proof. It is the same pattern as Willwacher’s simplified Deligne–Drinfeld proof and Angeltveit’s Smith–Toda paper posted the same day.
Sources
5 sources from 3 sites. Numbers match the chips in the text.
5 sources: 4 primary, 1 reaction
Primary
- arXiv 2610.23853: Brennan’s Conjecture and the Universal Integral Means Spectrum (Binder, Ivrii, Prause, Smirnov)arxiv.org, paper
- OpenAI math release: Brennan’s conjecture and sharp inverse-square integral means (family 072, PDF)github.com, paper
- OpenAI math release: A strict inverse-first-power bound for univalent functions (family 072, PDF)github.com, paper
- OpenAI math release: Lean scope note for family 072github.com, code
Reactions
- Wikipedia: Brennan conjectureen.wikipedia.org, discussion
Changes
- Filed (arXiv announcement of 19 Oct; PDF and OpenAI repo read)