Capacity Atlas Channel-capacity problems
Machine-checked mathematics

Lean formalizations

Capacity Atlas accepts Lean formalizations only. The status labels say exactly how much has been checked.

5entries with Lean work0 complete capacity proofs
Current policy

One proof assistant, shared definitions

New formalizations must compile with the pinned Lean toolchain, contain no sorry, and reuse the common channel and code definitions whenever the model fits them.

Status ladder

What each badge means

0

Not started

No Lean artifact is linked.

1

Definitions

The channel model or instance compiles and its basic well-formedness obligations are proved.

2

Statement

The exact capacity or bound is stated against the shared definitions.

3

Partial proof

At least one substantive achievability, converse, or supporting theorem is checked.

4

Complete proof

The advertised capacity result follows with no unproved axioms or placeholders.

Shared library

Common definitions live once

The initial Lean library defines finite stochastic channels, serial composition, one-shot codes, standard binary channels, and a reusable multiple-unicast index-coding instance.

FiniteChannel.leanStochastic kernels, identity, and serial composition Code.leanOne-shot encoders, decoders, success and error Channels/Binary.leanBSC, BEC, and Z-channel definitions Network/IndexCoding.leanMultiple-unicast instances and Sun-Jafar 11

Review rules

  • No sorry, admit, or undocumented axioms.
  • The data entry names every linked declaration.
  • Definitions state the same assumptions as the web page.
  • CI builds the complete Lean project.
  • A proof badge is upgraded only with the relevant theorem.
Dashboard

Formalization by problem

Submit a formalization →
ProblemCapacity statusLean statusFiles
Binary deletion channelChannels with memory open Lean: not started 0
Binary erasure channelPoint-to-point solved Lean: definitions 1
Binary symmetric channelPoint-to-point solved Lean: definitions 2
Binary Z-channelPoint-to-point solved Lean: definitions 1
Degraded discrete memoryless wiretap channelSecurity solved Lean: not started 0
Finite discrete memoryless channelPoint-to-point solved Lean: definitions 2
General discrete memoryless relay channelMulti-user open Lean: not started 0
Physically degraded two-receiver broadcast channelMulti-user solved Lean: not started 0
q-ary symmetric channelPoint-to-point solved Lean: not started 0
Real additive white Gaussian noise channelPoint-to-point solved Lean: not started 0
Sun-Jafar 11-message multiple-unicast index-coding instanceNetwork coding open Lean: definitions 1
Two-user discrete memoryless multiple-access channelMulti-user solved Lean: not started 0