VibeMathedMath problems solved with AI

The Courtade-Kumar conjecture: dictators are the most informative Boolean functions

Let XX be uniform on {0,1}n\{0,1\}^n and let YY be XX passed through independent binary symmetric channels with crossover probability ε∈[0,1/2]\varepsilon\in[0,1/2]. Kumar and Courtade (2013, 2014) conjectured that for every Boolean function f:{0,1}n→{0,1}f:\{0,1\}^n\to\{0,1\}, I(f(X);Y)≤1−h2(ε)I(f(X);Y)\le1-h_2(\varepsilon) bits, the value attained by a dictator f(x)=xif(x)=x_i. Partial results covered high-noise ranges (Ordentlich-Shayevitz-Weinstein, Samorodnitsky, Yu), balanced functions in ranges, and coordinatewise sums (Courtade-Kumar; Javanmard-Woodruff). Does every Boolean function satisfy I(f(X);Y)≤1−h2(ε)I(f(X);Y)\le1-h_2(\varepsilon) for every nn and every ε\varepsilon?

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Argument
Field
Boolean functions; information theory
Posed by
Gowtham R. Kumar and Thomas A. Courtade, Which Boolean functions are most informative? (ISIT 2013); Courtade and Kumar (IEEE Trans. IT 2014)
Year posed
2013
Years open
13y
Solved
2026-09-24
Model
Unreleased internal OpenAI model
Vendor
OpenAI
Collaborators
—
Verification
Lean-checked, statement unaudited
Publication
Announced
Collection
OpenAI math release (October 2026), version adc7f12
Significance
40 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Claims Theorem 1.1: for every nn, every soft channel u:{±1}n→[−1,1]u:\{\pm1\}^n\to[-1,1] and ρ∈[−1,1]\rho\in[-1,1], I(Tρu)≤ψ(∣ρ∣ψ−1(I(u)))I(T_\rho u)\le\psi(|\rho|\psi^{-1}(I(u))), with soft coordinates attaining equality; Corollary 1.2 gives I(f(X);Y)≤1−h2(ε)I(f(X);Y)\le1-h_2(\varepsilon) bits for Boolean ff, plus a strictly better bound when ff is biased; Theorem 1.3 is a mean-dependent entropy-production inequality. It does NOT treat non-uniform inputs, asymmetric noise, or multi-bit summaries. Independent proofs of the Boolean inequality were announced in September 2026 by Chen-Gohari-Javanmard-Lin-Mirrokni-Nair-Woodruff, Ky-Tran and Mahdavifar-Beirami.

What the AI did

The release README says the manuscripts were produced by an unreleased internal OpenAI model, the vast majority by one fixed procedure using on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier results produced by the models. Its named exceptions to that procedure (the zeta zero-free region work, whose Re(s) > 11/12 write-up was human edited, and the Hodge conjecture for CM abelian varieties) do not concern this family. Both manuscripts of the family are credited to OpenAI with no human author named. The principal manuscript follows the local-to-global differential-equation program of Chen-Gohari-Nair, credited to them; the Hellinger companion's source-lineage file says its arithmetic certificates are part of the proof.

Verification

No independent mathematician has checked this yet. Theorem 1.1 and Corollary 1.2 of the principal manuscript were read against the conjecture: the Boolean specialization gives I2(f(X);Y)≤1−h2(ε)I_2(f(X);Y)\le1-h_2(\varepsilon), with dictators attaining it. formalization.yaml lists ComparatorChallenges/CourtadeKumar.json, declaration OAI.LeanBlast.CourtadeKumar.courtadeKumarAndAttainment, file OAI/InformationTheory/BooleanNoise/Main.lean. The statement was read here: for n≥1n\ge1, 0≤ε≤1/20\le\varepsilon\le1/2 and every ff on the cube, the mutual information (defined from the bit-flip kernel, in bits) is at most 1−h(ε)1-h(\varepsilon), and dictators and anti-dictators attain it. That is exactly the conjecture. A second challenge, SoftChannel204.json (OAI.SoftChannel204.fullMain, solution module present, not in formalization.yaml, found via lean/docs/119.md), states the soft-channel Theorem 1.1, the bias-refined bound and the entropy-production inequality; read, not rebuilt. Permitted axioms are propext, Quot.sound and Classical.choice. Not rebuilt here. The manuscript itself cites four other recent preprints announcing proofs, one dated 21 September 2026, before this one.

Sources

Changelog1 change

Discussion