A community-maintained atlas of channel capacities, open gaps, and Lean formalizations.
Every entry separates literature claims from machine-checked Lean proofs.
Each page fixes the model, rate convention, best bounds, provenance, and what would count as progress.
Each input bit is independently deleted without an erasure marker. The exact capacity is unknown for every nontrivial deletion probability.
Each bit is independently flipped with probability p. This is the canonical finite noisy channel.
A relay assists communication from a source to a destination. Decode-forward and the cut-set bound do not coincide in general.
The power-constrained real Gaussian channel has a closed-form capacity attained by a Gaussian input.
This is the smallest multiple-unicast instance identified by Sun and Jafar where Shannon inequalities do not give the best known converse.
Inputs, outputs, transition law, side information, constraints, error criterion, and normalization are explicit.
Every achievability and converse has its own method, conditions, year, and references.
Open entries explain the bottleneck and list concrete results that would move the state of the art.
Definitions, statements, partial proofs, and complete proofs are distinct statuses. No badge hides a missing theorem.
Channel definitions live in shared modules. Contributions should reuse those definitions, contain no sorry, and name the exact theorem that has been checked.