QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit c681192368c2 Build record

Quantum Lean ecosystem

One reading map, honest dependency boundaries

QuantumComputinglib brings ASPBE declarations, selected external quantum-formalization references, and textbook explanations into one map. “Indexed” does not mean “imported”: every row states how the source is used.

Libraries represented in QuantumComputinglib

ASPBE

State preparation, block encoding, finite circuit semantics, construction routes, resource records, automation, and certified cases.

Built here

Mathlib

Finite types, matrices, algebra, norms, finite sums, and proof infrastructure used by the local Lean package.

Imported

quantum-computing-lean

Named states, gates, projectors, gate actions, decompositions, and compact finite-dimensional module organization.

Reference atlas

Lean-QuantumInfo

Finite-dimensional quantum and classical information, channels, distributions, entropy, and capacity.

Reference atlas

lean-quantum

Quantum states, channels, qudits, operator conventions, and higher-level quantum-information semantics.

Reference atlas

Lean-QuantumAlg-Bench

Pinned quantum-algorithm benchmark statements. They are useful formalization targets but unresolved statements are excluded from proof memory.

Benchmark reference

Lean-QIT-Bench

Pinned quantum-information benchmark statements for future QIT coverage; statement presence is not a local theorem certificate.

Benchmark reference

ATLAS v1

A pinned external memory over broad textbook mathematics. ASPBE preserves upstream compilation and quality distinctions, then admits only narrow locally compiled adapters.

External memory

How an external result enters the library

  1. Reference. Record the upstream repository, license, module, and exact declaration.
  2. Adapter. State the narrow ASPBE bridge without copying incompatible APIs.
  3. Compile. Import or prove the adapter under the pinned toolchain.
  4. Teach. Add the formula, plain-language reading, assumptions, and source link.

This prevents a survey entry, benchmark statement, or upstream theorem card from appearing as a locally compiled result. Before adding foundational QIT objects, search these sources and prefer one reviewed adapter/shared node to a parallel local definition.