I'm happy to share that we have completed a proof of the Most Informative Boolean Function conjecture (a.k.a. Courtade–Kumar conjecture) in full generality, resolving a longstanding central open problem at the intersection of information theory and Boolean function analysis (arxiv.org/abs/2609.24931). We have also successfully verified analytic parts of the proof in Lean. This result emerged from an extensive human–AI collaboration with input from multiple AI models developed through a close partnership between our group at Google with Amin, Chandra, and Zijie at CHUK; See section 4 for details on our human-AI collaboration. The Courtade–Kumar conjecture was among the problems we set out to tackle in our AI-acceleration paper (arXiv:2602.03837). In this effort, we made substantial use of the Stellar Colosseum harness (arXiv:2609.15983) and a range of external and internal Gemini models. Background and Significance of CK Conjecture: - Posed by Thomas Courtade and P. R. Kumar ("Which Boolean Functions Maximize Mutual Information on Noisy Inputs?"), the conjecture posits that for a uniform input X in {-1, 1}^n passed through BSC(p) to produce Y, the mutual information I(f(X); Y) for any Boolean function f is maximized by coordinate projections f(x) = x_i, attaining the sharp upper bound 1 - h(p). - The conjecture belongs to a broader family of extremal problems that have attracted sustained attention. It has helped motivate parallel lines of work in information theory, theoretical computer science, Boolean function analysis, and discrete isoperimetry. - Kindler, O’Donnell, and Witmer document the considerable interest it has generated, and Yu and Tan’s 2022 monograph describes it as “one of the most important open problems in information theory” [28, Section 9.1.2]. - At a structural level, the conjecture is connected to foundational isoperimetric and functional inequalities, including Talagrand’s isoperimetric inequality and Bobkov’s inequality, as well as related conjectures on their optimal forms. In some regimes, it also recovers Harper's classical edge-isoperimetric inequality on the discrete cube. Last week, we learned that Ky and Tran had independently obtained a very different proof of the conjecture. We coordinated with them to release the two works separately citing the other. The two approaches offer substantially different approaches (arxiv.org/abs/2609.24184). Congratulations to Ky and Tran  as well on this great achievement. Stellar Colosseum is available externally as the long proof pattern of /teamwork in AntiGravity (antigravity.google/blog/team…). We plan to move the math x human collaboration features to AntiGravity and I am excited to provide this as a math collaboration platfom externally. Thanks for my wonderful coauthors Zijie Chen, Amin Gohari, @AdelJavanmard, Honghao Lin, Chandra Nair David Woodruff Link to paper: arxiv.org/abs/2609.24931

I’m proud to share our latest milestone. Following our Google I/O demo, we’ve pushed our Antigravity agent, /teamwork (powered by Gemini) from a helpful assistant into a true research partner from CS theory to high-performance coding and hardware simulation. Here is what we’ve been building 👇 antigravity.google/blog/team… 🔹 Designed a cycle-level RISC-V CPU simulator with minimum human intervention that successfully boots an OS to shell (< 1% average error vs. golden reference)💻⚙️ 🔹 Math & TCS (via Long-proof Pattern): We hit 71% on TCSBench and solved multiple open problems—including sparse convex optimization (JMLR), subspace approximation (FOCS), provable LLM quantization, vector embeddings, and Prefix-Matrix Factorizations. We also generated a simplified construction of Knuth’s Cycles Conjecture (verified in Lean) and a reproof of the Erdős Unit Distance Problem. 🧮🧠 🔹 Open Source: /teamwork writes production code. We landed performance optimizations directly into major C++ libraries, including ParlayHash and up to a 32× speedup in Eigen. ⚡🚀 What excites me isn't just the benchmarks—it's our shift from Thinking Graphs to Graph Engineering. We’ve moved past rigid prompt engineering and sequential flows. /teamwork treats long-horizon research as a dynamic execution graph: decoupling agent specifications from orchestration logic, running parallel tournament synthesis trees, and dynamically adjusting agent topologies at runtime as complex problems unfold. 🕸️🤖 We’re releasing several new harness patterns today to solve a variety of problems (iterative coding, document review, Long Proof, and Aletheia). I'm thrilled our team can share these agents via AGY with our users. Stay tuned for more! Read the full technical deep-dive on the blog here: antigravity.google/blog/team… #AI #Gemini #AI4Systems #AI4Math #AI4Science #ComputerArchitecture #Systems #FormalVerification #OpenSource