Courtade–Kumar ‘most informative Boolean function’ conjecture (2013) proved three times in two days, all with AI: Ky & Tran (ChatGPT), Google + CUHK (Gemini, Lean-verified end-to-end), Mahdavifar & Beirami
Event confirmedAwaiting review
Importance: major (4 of 5)The takeaway
A central 2013 conjecture of information theory, that one input bit (a dictator) keeps the most information through noise, fell to three independent proofs on 21–22 Sep 2026. All three teams disclose AI help; Google’s 250-page proof says ‘the overwhelming majority of the novel ideas’ came from AI and is checked end-to-end in Lean.
Status
- Claim
Event confirmedAwaiting review
- Our reporting
- High confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 9 October 2026
Your AI and this story
- GPT-6 Astra144 days after its cutoff
- Claude Opus 5.583 days after its cutoff
- Gemini 3.8 Flash174 days after its cutoff
- Grok 4.7113 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 83 days before it.
Key facts
- Statement: for X uniform on {−1,1}^n and Y obtained by flipping each bit independently with probability p, every Boolean f satisfies I(f(X); Y) ≤ 1 − h(p), with equality for dictators (Courtade & Kumar, ISIT 2013; IEEE Trans. Inf. Theory 2014)
- Ky & Tran (FPT University; USTC), arXiv 2609.24184, posted 21 Sep 2026 06:56 UTC, 36 pages. Disclosure: ‘The authors formulated the approach and used ChatGPT to develop the proofs, prepare the verification code, and revise the exposition.’ Ky told VnExpress AI helped ‘quickly test ideas and identify counterexamples’
- Chen, Gohari, Javanmard, Lin, Mirrokni, Nair & Woodruff (CUHK + Google), arXiv 2609.24931, v1 21 Sep 2026 17:26 UTC, v2 24 Sep (added the Lean link and concurrent work). Abstract: ‘The entire proof, including all numerical certificates, has been formally verified in Lean end-to-end’
- Google paper, Part 4 ‘Human–AI collaboration’: Gemini in the Stellar Colosseum framework first found counterexamples to a generalised version (Conjecture 5) of the CUHK reduction; CUHK then supplied the ‘max-phi Bellman function’, reducing the conjecture to a 14-variable optimisation; ‘The AI then led the effort to partition the space into different regions, developing novel, non-trivial theoretical ideas and numerical interval arithmetic calculations’; the move from the balanced to the unbalanced case ‘operated entirely without human input’; ‘Additional ideas, verification, and critiques were contributed by human collaborators working with Anthropic and OpenAI models’
- Stellar Colosseum (Lin, Woodruff, Deng, Mao, Zuo, Mirrokni; arXiv 2609.15983, 14 Sep 2026) is a many-agent harness; Google says it is available externally as the ‘Long Proof’ pattern in Antigravity Teamwork
- Mahdavifar & Beirami, arXiv 2609.26444 (v1 22 Sep, v2 28 Sep), also prove multibit extensions. Disclosure: ‘The proof of the single-bit result, including its detailed mathematical derivations, was generated by generative AI systems; the authors’ role was high-level direction, feedback, and final review. The multibit extension was entirely human-directed’
- OpenAI’s 6 Oct catalogue, family 119 (manuscripts dated 24 Sep), claims the Courtade–Kumar conjecture and the Hellinger conjecture with arbitrary output bias. On 7 Oct Ky posted a separate paper proving the balanced Hellinger conjecture for antipodal Boolean functions (arXiv 2610.10618), citing all of these
- Reception: Google Research VP Vahab Mirrokni announced the Google proof on X, called the conjecture a ‘longstanding central open problem at the intersection of information theory and Boolean function analysis’ and congratulated Ky and Tran (VietNamNet, VnExpress); the two teams coordinated a simultaneous release
What happened
The Courtade–Kumar conjecture asks how much a single bit can say about a noisy copy of its input. Courtade and Kumar conjectured in 2013 that the best one-bit summary is simply one of the input coordinates. Partial results covered high noise, balanced functions and weaker forms, and Google listed it in its February 2026 “Accelerating scientific research with Gemini” paper as a problem it was trying to solve with AI.
On 21 September 2026 Vu Khac Ky (FPT University) and Tuan Tran (USTC) posted a 36-page proof. The same day a Google–CUHK team posted a roughly 250-page computer-assisted proof. Its Part 4 describes the collaboration: Gemini, running in Google’s Stellar Colosseum many-agent harness, first found counterexamples to an over-general version of CUHK’s earlier reduction. CUHK then supplied the right Bellman function, after which “the AI then led the effort”, partitioning a 14-variable domain into regions and proving bounds with interval arithmetic. The authors write that “the overwhelming majority of the novel ideas and results in this paper were generated by AI”, and that the whole proof, numerical certificates included, is checked by Lean’s kernel. A day later Hessam Mahdavifar and Ahmad Beirami posted a third proof whose single-bit part was, by their account, generated by AI.
The two first teams coordinated their release. OpenAI’s 6 October catalogue later included the same conjecture (family 119, manuscripts dated 24 September).
Why it matters
This is one of the clearest cases of AI-driven results arriving simultaneously from several directions: a lab team with its own agent harness, a two-person academic team using ChatGPT, and a third team, all within about 30 hours. For a model with an older cutoff: the Courtade–Kumar conjecture should now be treated as proved, with a machine-checked proof.
What is disputed or not yet verified
| Verification | Google–CUHK proof formally verified end-to-end in Lean (per the authors); the others are unrefereed preprints |
|---|
Sources
8 sources from 4 sites. Numbers match the chips in the text.
8 sources: 6 primary, 2 press
Primary
- Chen, Gohari, Javanmard, Lin, Mirrokni, Nair, Woodruff: A Proof of the Most Informative Boolean Function Conjecture (arXiv 2609.24931)arxiv.org, paper
- Ky & Tran: Dictators are most informative (arXiv 2609.24184)arxiv.org, paper
- Mahdavifar & Beirami: The Most Informative Bit and Beyond (arXiv 2609.26444)arxiv.org, paper
- Lin et al.: Stellar Colosseum, a many-agent harness for long-horizon research (arXiv 2609.15983)arxiv.org, paper
- Ky: The Hellinger Conjecture for Antipodal Boolean Functions (arXiv 2610.10618, 7 Oct)arxiv.org, paper
- OpenAI math catalogue (CONTENTS.md, family 119)github.com, paper
Press
Changes
- Filed (missed in September; found through a citation in arXiv 2610.10618). PDFs and disclosures read