Browse › Theoretical computer science › 119 The Courtade–Kumar and Hellinger conjectures
Hellinger contraction with arbitrary Boolean output bias
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove the Hellinger conjecture for Boolean functions on the uniform discrete cube, with arbitrary output bias. For a Boolean function of mean m and every $\rho\in[-1,1]$, the loss $\sqrt{1-m^2}-\mathbb E\sqrt{1-(T_\rho f)^2}$ is at most $1-\sqrt{1-\rho^2}$, with equality for signed coordinates. The proof combines asymmetric dimension induction, a calibrated noise-semigroup energy estimate, and finite exact arithmetic certificates. The Hellinger inequality also yields the Courtade–Kumar information bound.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Follow-up works
- V. K. Ky, The Hellinger Conjecture for Antipodal Boolean Functions (arXiv:2610.10618, 7 Oct 2026). Gives a spectral proof of the balanced Hellinger inequality for antipodal (sign-reversing) Boolean functions and extends it to arbitrary independent binary-input channels; Section 1.2 cites OpenAI's family-119 entry as an announcement of the Hellinger inequality for arbitrary output bias, without verifying it.
Formalization
- OpenAI math release, Lean scope notes for family 119: The Courtade–Kumar and Hellinger conjectures (lean/docs/119.md, 2026). The family's Lean development covers only the companion paper's soft-channel and Courtade–Kumar results and does not cover this paper's Hellinger inequality. [family-level]
- D. P. Woodruff et al., general-courtade-kumar-lean (GitHub, release v1.2 dated 2026-10-01). An independent Lean 4 proof of the Courtade–Kumar inequality, which this paper derives as a corollary of the Hellinger inequality; it accompanies arXiv:2609.24931 and does not formalize the Hellinger inequality.
Related prior literature mentioned by others
- P. Durcik, M. Fraccaroli and J. Roos, A weak Hellinger inequality for noisy Boolean channels (arXiv:2609.28534, v1 22 Sep 2026, v2 29 Sep 2026). Cited by Ky's follow-up; proves the Hellinger inequality of Theorem 1.1 for Boolean functions with any mean but with the full noisy output $Y$ replaced by a one-bit statistic $g(Y)$, computer-assisted and formalized in Lean 4.
Digests and expositions
- AI Proved What?, The best bit? The Courtade–Kumar and Hellinger conjectures (Episode 119, October 2026). This AI-assisted video and transcript explain both manuscripts’ claims and proof strategies and distinguish the contraction paper’s Lean scope from the Hellinger paper’s exact-arithmetic certificates. [AI-generated per source] [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 119
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:Hellinger-contraction-with-arbitrary-Boolean-output-bias-September-24-2026,
author = {{OpenAI}},
title = {{Hellinger contraction with arbitrary Boolean output bias}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/Hellinger-contraction-with-arbitrary-Boolean-output-bias-September-24-2026/main.pdf}{OAI:Hellinger-contraction-with-arbitrary-Boolean-output-bias-September-24-2026}},
year = {2026}
}From OpenAI's README for this paper:
Verification
The exact arithmetic checks require Python 3.9 or later with SymPy 1.14.0 and
a C++ compiler supporting signed __int128, such as GCC or Clang. Run with
assertions enabled; do not use Python's -O option or set PYTHONOPTIMIZE.
From this paper directory, run:
verification_output="$(mktemp -d)"
python3 verification/verify_all.py --output-dir "$verification_output"
The output directory must be new or empty. Success is exit code zero, a final
PASS, and "status": "pass" in verification.json under that output
directory. The runner records source hashes, commands, and separate logs. It
does not install dependencies or use network access. Use --cxx clang++ to
select Clang when needed.
Lean formalization
OpenAI provides Lean files for this family: lean/docs/119.md. The Lean statements have not been checked by people against the paper's claims.
Family 119: The Courtade–Kumar and Hellinger conjectures
Proves the Courtade–Kumar conjecture: among Boolean functions of independent uniform bits, a single coordinate retains the most mutual information after independent bit-flip noise. A stronger theorem treats randomized binary summaries at fixed initial information. The Hellinger conjecture is also proved for every Boolean output bias and noise correlation.
Other papers in this family:
- Sharp binary-information contraction on the discrete cube · September 24, 2026