Google-led team proves Courtade–Kumar conjecture in full, with AI and Lean
RexDouglass · x · 2026-09-22
A Google group with CUHK collaborators announced a complete, computer-assisted proof of the Most Informative Boolean Function (Courtade–Kumar) conjecture, posted to arXiv (2609.24931). The proof uses the differential-equation method, reduces entropy production to an unrestricted Bellman inequality with mean and entropy constraints, and shows I(g(X);Y) ≤ 1 − H₂(p) with dictator functions as equality. Analytic parts were verified in Lean, emerging from extensive human–AI collaboration with multiple Gemini models via the Stellar Colosseum harness.
More from Research
- MatBrain splits reasoning from tool use: two models screen 30,000 crystal candidates in 48 hours — bravo_abad · 2026-09-23
- Scale AI launches SWE-Bench Pro V2, a harder agentic coding benchmark — bigblueboo · 2026-09-23
- If AI Writes All the Papers, Peer Review Becomes Humanity's Remaining Role — sudoraohacker · 2026-09-23
- Yarin Gal: I Ignore Papers Where the Candidate Isn't First or Last Author — yaringal · 2026-09-23
- New paper: Transferring the Intelligence of VLMs to Robotic Control — _akhaliq · 2026-09-23
- NTU UMM study: generation training boosts understanding in native multimodal models, but naive sharing conflicts — jiqizhixin · 2026-09-23