where
is mutual information, is binary Shannon
entropy, with taken to equal 0, and where is measured in bits. This convention
agrees with the limit of as .
Equality holds for .
Proofs of the conjecture were given by Chen et al. (2026a), Ky and Tran (2026), Kramer and Saglam (2026), and Mahdavifar and Beirami (2026). The result holds without
requiring
to have expectation value zero. Chen et al.
(2026b) provide a Lean formalization with published records of completed kernel
checking and acceptance by the separate con-leche checker.
OpenAI (2026) proved the stronger inequality
where
is any random variable jointly distributed with
, the channel reversals are independent
of ,,
and
for . Here is the increasing inverse
function. Equality is attained by channels with conditional
expectation for .
Taking
implies the conjectured bound, including for biased outputs. This stronger form also
follows by integrating the entropy-production inequality of Chen et al. (2026a).
MathVet (2026) published a separate successful Lean-kernel check of OpenAI's formalized
contraction theorem and its definitions, allowing only Lean's standard axioms.
and a Boolean function 
, let 
have the uniform distribution
on 
and put 
with independent signs 
, also independent
of 
, and 
for 
.
The assertion is
is mutual information, 
is binary Shannon
entropy, with 
taken to equal 0, and where 
is measured in bits. This convention
agrees with the limit of 
as 
.
Equality holds for 
.
to have expectation value zero. Chen et al.
(2026b) provide a Lean formalization with published records of completed kernel
checking and acceptance by the separate con-leche checker.
is any random variable jointly distributed with
, the channel reversals are independent
of 
, 
,
and 
for 
. Here ![psi^(-1):[0,1]->[0,1]](/images/equations/Courtade-KumarConjecture/Inline24.svg)
is the increasing inverse
function. Equality is attained by channels with conditional
expectation ![E[U|X]=aX_i](/images/equations/Courtade-KumarConjecture/Inline25.svg)
for 
.
Taking 
implies the conjectured bound, including for biased outputs. This stronger form also
follows by integrating the entropy-production inequality of Chen et al. (2026a).
MathVet (2026) published a separate successful Lean-kernel check of OpenAI's formalized
contraction theorem and its definitions, allowing only Lean's standard axioms.
