AI Proof WatchKeep up with AI contributions

Three Conjectures on Binary Channels for the Doubly Symmetric Binary Source

Georg Pichler

For a doubly symmetric binary source with crossover p∈[0,1], the convex hull of rate triples from arbitrary binary channels equals that from binary symmetric channels. At p=0 and parameters a,d∈(0,1), no binary channel pair with rates no larger than the stated Z/S pair has greater I(U;V), and no pair with rates at least those of the stated Z/Z pair has smaller I(U;V). These are value bounds, not uniqueness claims.

Sources for this record

What was already known

Pichler and coauthors posed the convex-hull equality; only endpoint cases were known. Dikshtein, Ordentlich and Shamai posed the two p=0 optimality claims with numerical evidence.

AI involvement AI-centered

Georg Pichler posed or coauthored the earlier questions, directed the project, reviewed the proof architecture and later explained all three proofs. He credits Claude Opus 5 with almost the entire original Lean development and Claude Fable 5.1 with a certificate-checking method. Individual lemma credit is not fully resolved.

Pichler's paper credits Claude Opus 5 with almost the entire original Lean proof development for three previously open claims, under his direction; Claude Fable 5.1 supplied a retained certificate-checking method.

Importance Notable

Establishes three previously proposed binary-channel value claims within their exact channel and parameter scope.

Limitations

The last two results assert optimal values, not unique optimizers. Extending from binary to unrestricted output alphabets uses cited cardinality reductions outside this Lean development.

Technical verification Formal (Lean 4/Mathlib kernel, including exact interval and Pólya certificate computation)

All three compared statements are reported proved with only standard Lean axioms; the two computational certificates on the Conjecture 1 path run in the kernel. The prior binary-output reduction and objective translation for Conjecture 2 are cited, not formalized.

Formal checking

Lake build and #print axioms across the proof path, including kernel evaluation of the 88-cell sweep and 24129-coefficient certificate

Checker
Lean 4 kernel
Scope
averaged_bsc_maximise_mutual_information, conjecture1_p0 and conjecture2_p0 for binary channels
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Full

Pichler's later paper explains the central even/odd decomposition, interior-optimizer and saddle arguments, and corner certificates for all three claims; his MathOverflow answer also explains the first proof's mechanism. The paper text had AI drafting assistance, but he presents and accepts the account.

Correction and publication history

2026-10-18 · publication

Establishes three previously proposed binary-channel value claims within their exact channel and parameter scope.

Read this published revision