QuantumComputinglib learn · inspect · formalize
Checked on this commit 2,822 public declarations commit 274beb0387ea Build record

Formal quantum computing, read alongside Lean

QuantumComputinglib

QuantumComputinglib is the textbook and declaration browser for ASPBE. ASPBE studies two different construction problems. State preparation asks a unitary to produce one target state. Block encoding asks a larger unitary to expose a target operator through a clean ancilla block. This site keeps their contracts, proof routes, and completion status separate.

Start with state preparation Study block encoding See the full reading guide →

Choose the problem first

Two applications, two acceptance contracts

The problems share finite matrix foundations and the same proof discipline, but neither is presented as a special case of the other.

Application 1

State preparation

\[U|0^n\rangle=|\psi\rangle\]

Fix a normalized target state, construct a unitary, and prove that its action on the all-zero state gives exactly those amplitudes.

Read the state-preparation route →

Application 2

Block encoding

\[\Pi U\Pi^\dagger=A/\alpha\]

Fix an operator, normalization, ancilla convention, and register order; then prove that the projected block of a larger unitary has the requested value.

Read the block-encoding route →

State-preparation workflow

From a target vector to a preparation certificate

Normalization, unitarity, and state action are separate obligations. The first-column identity is the matrix form of the same state-action equation.

State-preparation proof and export flow editable Mermaid source 
flowchart LR
  T["Target state<br/>|ψ⟩"] --> N["Check normalization<br/>⟨ψ|ψ⟩ = 1"]
  N --> C["Choose a circuit<br/>or unitary completion"]
  C --> U["Prove U is unitary"]
  C --> A["Prove the state action<br/>U|0ⁿ⟩ = |ψ⟩"]
  U --> L["Lean state-preparation<br/>certificate"]
  A --> L
  L --> E["Export one certified<br/>finite instance"]

  classDef target fill:#ffffff,stroke:#6b6045,color:#222222,stroke-width:1.5px;
  classDef work fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px;
  classDef proof fill:#ffffff,stroke:#2f7355,color:#18382b,stroke-width:1.5px;
  class T,N target;
  class C,U,A work;
  class L,E proof;

Block-encoding workflow

From an operator contract to a clean-block certificate

This route introduces choices that state preparation does not need: ancilla count, a clean projector, register layout, normalization \(\alpha\), and an exact or approximate block norm.

Block-encoding proof and export flow editable Mermaid source 
flowchart LR
  T["Target operator A<br/>and scale α"] --> R["Fix ancillas, norm,<br/>and register order"]
  R --> C["Choose a construction<br/>family and unitary U"]
  C --> U["Prove U is unitary"]
  C --> B["Prove the clean block<br/>‖A − α Π U Π†‖ ≤ ε"]
  U --> L["Lean block-encoding<br/>certificate"]
  B --> L
  L --> E["Export and check one<br/>certified finite instance"]

  classDef target fill:#ffffff,stroke:#49677d,color:#1f2e39,stroke-width:1.5px;
  classDef work fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px;
  classDef proof fill:#ffffff,stroke:#2f7355,color:#18382b,stroke-width:1.5px;
  class T,R target;
  class C,U,B work;
  class L,E proof;

Current checkout

What this build actually certifies

2,822explicit public declarations
1,788source docstrings
395experimental declarations
0explicit incomplete proofs
9guided learning chapters

Compiled means the Lean and test gates passed on commit 274beb0387ea. A contract record may compile even when a concrete construction route is still partial; the site shows those two statuses separately.

Shared evidence discipline

What happens after either contract is fixed

ASPBE explores candidates, records why routes fail, and lets Lean decide formal promotion. A Qiskit check is useful finite evidence after certification; it does not prove a symbolic family.

Shared certification and feedback loop editable Mermaid source 
flowchart LR
  C["Fixed mathematical<br/>contract"] --> O["Named proof<br/>obligations"]
  O --> P["Candidate routes<br/>with provenance"]
  P --> L{"Lean gate"}
  L -- "proof fails" --> F["Classified failure<br/>and next local lemma"]
  F --> P
  L -- "certificate compiles" --> X["Finite export<br/>and circuit check"]
  X --> D["Documented result<br/>with stated scope"]

  classDef contract fill:#f8f5ee,stroke:#826a32,color:#222222,stroke-width:1.5px;
  classDef process fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px;
  classDef gate fill:#edf5f1,stroke:#2f7355,color:#18382b,stroke-width:1.5px;
  classDef feedback fill:#fff2ef,stroke:#a44b3f,color:#4a2520,stroke-width:1.25px;
  class C contract;
  class O,P,X,D process;
  class L gate;
  class F feedback;

Use the project

Read, formalize, or submit a construction

The public site is not only a declaration catalog. It keeps the original user-facing task builder, the local-compilation workspace, and the reviewed contribution route beside the textbook.

Read

Learn from a checked chapter

Follow a formula from its physical meaning to the exact Lean declaration.

Open the book map →
Formalize

Compare LaTeX and Lean

Edit a theorem, inspect dependencies, and compile temporary code with the local companion.

Open the workspace →
Run

Build an ASPBE task packet

Describe a target state or operator, choose a harness, and export a reproducible task packet.

Open the task builder →

Project record

News and auditable priority

The dates below are repository milestones. They do not replace the generated proof-status pages.

  1. ASPBE and QuantumComputinglib.

    The two application tracks, local workspace, task builder, and contributor review path are presented in one site.

  2. Blueprint and Library Explorer.

    One generated inventory now drives the checked Blueprint catalog and searchable declaration browser.

  3. Public testing preview.

    The site exposed separate State Preparation and Block Encoding directions and the user task builder.

  4. Earliest repository record.

    The initial commit and timestamped manifest begin the public, auditable project history. No earlier date is asserted without evidence.

Reading guide

Follow one application without losing the shared foundations

Shared foundations

01 Vectors, matrices, and basis states Fix the finite matrix model, pointwise equality, dimensions, and resource records used by every later certificate. 02 Gates, unitaries, and circuit meaning Separate gate syntax from matrix evaluation and make register order an explicit part of the semantic boundary.

State preparation

03 The state-preparation problem Ask one concrete question: which unitary sends the all-zero basis state to the normalized state we want? 04 Reading and reusing a preparation certificate Connect the ket equation to a matrix column, package the proof, and reuse exact preparation where an approximate interface is expected.

Block encoding

05 The block-encoding contract State the block contract with normalization, explicit register layout, and a verifier-facing certificate record. 06 Construction routes and composition rules Reuse permutation, one-sparse, LCU, product, dilation, and QSVT interfaces instead of rediscovering each route per benchmark. 07 Certified block-encoding cases Distinguish completed local certificates from paper-facing contract models and historical experiments.

System and evidence

08 Candidate comparison and executable exports Keep formal validity lexicographically ahead of resource quality, then expose accepted candidates to executable tooling. 09 Search control, evidence, and open work Show how typed stages, agent layers, candidate populations, proof gates, and explicit open problems coordinate without overstating evidence.

Audit the source

Explanation, inventory, and checked Blueprint

The chapters teach selected results. The Library Explorer inventories every explicit public declaration. The Verso Blueprint resolves its Lean references during the build.

Implementation map Library Explorer Verso Blueprint Task builder →