About the project

An atlas for capacity questions

Capacity Atlas turns scattered formulas, bounds, and open problems into precise, reviewable, machine-readable research objects.

12seed entriesDesigned to grow through small pull requests

Make the frontier legible

A capacity result is meaningful only after the model is fixed. Feedback, state information, constraints, error criteria, code classes, and rate normalization can all change the answer. Capacity Atlas treats that full specification as the primary object.

For solved problems, the site records the exact answer and the achievability and converse behind it. For open problems, it records the best gap, why it persists, and what would count as progress.

Repository as source of truth

YAML data, references, Lean files, and build code live together. Git history records provenance.

Static by default

The public site is generated HTML. There is no database, account system, or application server to maintain.

Claims before polish

A small, auditable corpus is better than a large scraped list with ambiguous assumptions.

Formalization without theatre

The status ladder prevents a compiled definition from being mistaken for a proved capacity theorem.

GitHub provides the social layer

Pull requests change canonical entries. Issues hold corrections and scoped research discussions. GitHub history credits contributors. An optional giscus integration can later embed GitHub Discussions directly on problem pages without introducing a separate user database.

Built for humans and research agents

Every generated problem page also has a JSON representation. The complete index, reference database, and JSON Schema are available from the API page. This makes it possible to build search tools, benchmark generators, Lean task queues, or AI research packets without scraping HTML.

Deliberately narrow first milestones

  1. Expand the curated point-to-point and classical multi-user entries.
  2. Formalize finite entropy and mutual information on top of the shared channel core.
  3. State the operational finite-DMC capacity theorem precisely in Lean.
  4. Formalize elementary exact capacities before attempting difficult open converses.
  5. Enable GitHub Discussions and embedded per-problem comments once moderation is configured.