---
id: "2026-09-21-courtade-kumar-conjecture-proved"
url: "https://postcutoff.com/e/2026-09-21-courtade-kumar-conjecture-proved/"
as_of: "2026-10-09T19:24:00+02:00"
date: "2026-09-21"
date_precision: day
category: science
importance: 4
confidence: high
status: [Event confirmed, Awaiting review]
verification: Lean-verified
sources: 8
editor: Adam Bicz
human_review: null
version: null
---

As of: 2026-10-09 19:24 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz.
Canonical page: https://postcutoff.com/e/2026-09-21-courtade-kumar-conjecture-proved/

# 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

The Courtade–Kumar conjecture (Kumar & Courtade 2013) says that among all Boolean functions f of n uniform bits, a dictator f(x) = x_i maximises the mutual information I(f(X); Y) when Y is X passed through a binary symmetric channel. On 21 Sep 2026 two independent proofs appeared on arXiv: Vu Khac Ky and Tuan Tran's "Dictators are most informative" (2609.24184, 36 pages; "used ChatGPT to develop the proofs, prepare the verification code, and revise the exposition") and a ~250-page computer-assisted proof by Google (Mirrokni, Woodruff, Javanmard, Lin) and CUHK (Chen, Gohari, Nair) (2609.24931), which states that "the overwhelming majority of the novel ideas and results in this paper were generated by AI" (Gemini in Google's Stellar Colosseum harness) and that the entire proof, including numerical certificates, is formally verified in Lean end-to-end. A third proof by Mahdavifar & Beirami (2609.26444, 22 Sep) says its single-bit proof "was generated by generative AI systems". OpenAI's 6 Oct catalogue (family 119) also claims the conjecture.

## 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

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 144 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 83 days after its cutoff
- Gemini 3.8 Flash (training cutoff March 2026): 174 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 113 days after its cutoff

## Sources

1. [Chen, Gohari, Javanmard, Lin, Mirrokni, Nair, Woodruff: A Proof of the Most Informative Boolean Function Conjecture (arXiv 2609.24931)](https://arxiv.org/abs/2609.24931) (arxiv.org, paper)
2. [Ky & Tran: Dictators are most informative (arXiv 2609.24184)](https://arxiv.org/abs/2609.24184) (arxiv.org, paper)
3. [Mahdavifar & Beirami: The Most Informative Bit and Beyond (arXiv 2609.26444)](https://arxiv.org/abs/2609.26444) (arxiv.org, paper)
4. [Lin et al.: Stellar Colosseum, a many-agent harness for long-horizon research (arXiv 2609.15983)](https://arxiv.org/abs/2609.15983) (arxiv.org, paper)
5. [Ky: The Hellinger Conjecture for Antipodal Boolean Functions (arXiv 2610.10618, 7 Oct)](https://arxiv.org/abs/2610.10618) (arxiv.org, paper)
6. [OpenAI math catalogue (CONTENTS.md, family 119)](https://github.com/openai/math/blob/main/CONTENTS.md) (github.com, paper)
7. [VietNamNet: Vietnamese mathematicians find proof for decade-old information theory puzzle (29 Sep)](https://vietnamnet.vn/en/vietnamese-mathematicians-find-proof-for-decade-old-information-theory-puzzle-2559814.html) (vietnamnet.vn, press)
8. [VnExpress: Vietnamese mathematicians solve decade-old information theory problem (3 Oct)](https://e.vnexpress.net/news/tech/personalities/vietnamese-mathematicians-solve-decade-old-information-theory-problem-5125621.html) (e.vnexpress.net, press)

## Changes

- 2026-10-09 (filed): Created (missed in September; found through a citation in arXiv 2610.10618). PDFs and disclosures read

## Related

- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)
- 2026-09-30: [Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help](https://postcutoff.com/e/2026-09-30-ai-assisted-conjecture-wave-summer-2026/index.md)
- 2026-08-27: [Google's Antigravity 'Teamwork' multi-agent framework with Gemini 3.7 Flash solves seven open CS/math problems, incl. part of Knuth's cycles problem](https://postcutoff.com/e/2026-08-27-antigravity-teamwork-open-problems/index.md)