Part I
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 →QuantumComputingBench · open exercise book
A graph-grounded quantum-computing exercise book
Five parts. 198 retained native core IDs. Read substantial mathematics without Lean, then inspect the formal companion and exact evidence boundaries.
Read the mathematical exercises · Explore the Lean companion
Textbook edition in progress; semantic review and formal-view expansion remain explicit gates.
Human-understanding infrastructure for Math 2.0
QuantumComputinglib
Understand a quantum construction. Read its proof beside Lean. Follow the shared ideas and see exactly which assumptions it needs.
ASPBE constructs and certifies state preparation and block encoding. The library connects those certificates to readable mathematics, circuit figures and reusable proof graphs.
Part I · State Preparation
Part II · Block Encoding
Part III · QIT & Representation
Part IV · Scientific Computing
Parts I–II: core certificates and open routes. Parts III–IV: source-anchored curricula; local Lean certificates pending.
From checked results to shared understanding
Our place in Math 2.0
Terence Tao's Math 2.0 talk echoes our original aim: a living quantum textbook with inspectable proofs, reusable mechanisms and explicit model boundaries. We invite collaborators to improve the teaching and explore the potential of proof maps.
Foundations: a living knowledge network and a quality Lean library. Core value: clearer explanations and better interactive teaching. Research agenda: shared principles, ablations, theorem neighborhoods, auditable AI tools and model-failure analysis.
Nine contribution directions: what exists and what comes next →Choose the problem first
Four textbook parts, one shared Lean graph
Four peer parts share the same foundations. Within Parts I and II, the main construction relation is State Preparation → Block Encoding: PREPARE is a reusable subproblem inside many block-encoding routes. A block-to-state consumer path also exists, but it is not the inclusion relation and it needs extra branch, normalization and amplification hypotheses. Shared foundations are authored once rather than duplicated.
Part II
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 →Part III · Planned
Quantum Information and Representation Theory
States, channels and measurements lead to symmetry, Schur–Weyl duality and information-theoretic applications. Leditzky's notes anchor the curriculum; named local Lean roots are still required.
Explore the representation-theoretic QIT curriculum →Part IV · Planned
Quantum Algorithms for Scientific Computation
Lin–Wiebe's scientific algorithms reuse the shared Block Encoding part, then add transforms, simulation, estimation and application contracts.
Explore scientific quantum algorithms →flowchart TB
accTitle: QuantumComputinglib textbooks and shared Lean foundations
accDescr: External Lean references enter shared foundations only through reviewed reuse or narrow adapters. The textbooks reuse these foundations. State Preparation and Block Encoding are the current core; Quantum Information and Scientific Computing are planned extensions. Conditional algorithm and theory support lead into Scientific Computing. These are curriculum relationships, not Lean theorem implications.
EXT["External Lean references<br/>Mathlib · attributed quantum Lean libraries<br/>upstream references, not automatic local proofs"]
CORE["Shared Lean foundations<br/>Reviewed building blocks reused across textbooks<br/>linear algebra · states/tensors · operators<br/>circuits/registers · norms · resource interfaces"]
subgraph TEXTBOOK["QuantumComputinglib textbooks"]
direction TB
subgraph CURRENT["Current core · compiled guided chapters"]
direction LR
SP["Part I · State Preparation<br/>U|0^n⟩ = |ψ⟩"]
BE["Part II · Block Encoding<br/>‖A - αΠUΠ†‖ ≤ ε"]
end
subgraph PLANNED["Planned extensions · local chapter admission required"]
direction TB
QIT["Planned Part III · Quantum Information<br/>and Representation Theory<br/>symmetry · Schur–Weyl · de Finetti"]
SCI["Planned Part IV · Quantum Scientific Computing<br/>QSP/QSVT · simulation · estimation<br/>linear systems · dynamics · open systems"]
end
end
EXT -. "reviewed reuse / narrow adapters" .-> CORE
CORE -->|common foundation| TEXTBOOK
BE -. "algorithm support" .-> SCI
QIT -. "theoretical support" .-> SCI
classDef core fill:#f8f5ee,stroke:#826a32,color:#222222,stroke-width:1.5px;
classDef state fill:#edf5f1,stroke:#2f7355,color:#18382b,stroke-width:1.5px;
classDef block fill:#eef3f7,stroke:#49677d,color:#1f2e39,stroke-width:1.5px;
classDef future fill:#f7f4fb,stroke:#735a8f,color:#2f2440,stroke-width:1.5px;
classDef external fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px;
class CORE core;
class SP state;
class BE block;
class QIT,SCI future;
class EXT external;
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.
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.
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
4,524explicit public declarations
2,337source docstrings
395experimental declarations
0explicit incomplete proofs
9guided learning chapters
Compiled means the Lean and test gates
passed on commit 4e2c5b2c0be5. 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.
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.
Learn from a checked chapter
Follow a formula from its physical meaning to the exact Lean declaration.
Open the book map →Compare LaTeX and Lean
Edit a theorem, inspect dependencies, and compile temporary code with the local companion.
Open the workspace →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.
- QuantumComputingBench starts.
We are launching QuantumComputingBench to build graph-grounded QA for training and evaluating specialized quantum-computing models across knowledge, mathematical reasoning and Lean skills, with planned topics clearly separated from verified library evidence.
- Priority: digesting discovered reversible circuits.
We have opened a source-first formalization route for Gu, Kemeny, Yelin and Lukin, explicitly crediting the author Lean proofs and separating their adaptation from circuit, error and resource closure. Read the layered Uncompute plan →. Work in progress; no paper-wide or new local certificate is claimed.
- Four textbooks you can browse, not just a roadmap.
All four peer textbooks have homepage actions, a shared curriculum diagram and chapter-map entries. The textbook explorer filters chapters by book, technique and evidence status, with reading sources and expandable commit-pinned OpenAI Math memory. Parts III and IV remain source-anchored plans, not newly certified Lean books. The first curriculum release was merged in PR #87; rendering and deployed-reader checks were repaired in #88 and #89.
- Four peer textbook parts and explicit formalization plans.
State Preparation and Block Encoding are joined by Quantum Information and Representation Theory, and Quantum Algorithms for Scientific Computation. Walsh-series and diagonal-operator papers have source-linked plans and reusable technical cards. New parts and upstream OpenAI Math placements are planned curriculum, not new local theorem certificates.
- Statement Seal, evidence memory, and proof digestion.
QuantumComputinglib now freezes source-facing quantum contracts before proof search, types and salvages failed routes before cleanup, keeps environment/API failures separate from mathematical refutation, defaults routine coordination to deterministic/low-token control in light of local route-ablation evidence, requires distinct uncertainty for parallel Workers, and seals PURIFIED reader explanations against the source and Lean graphs.
- Schrödingerisation smooth auxiliary-state preparation: a structured logical resource bound.
The smooth auxiliary \(p\)-register state required by Jin–Liu–Ma’s PDE Schrödingerisation construction, viewed alongside the smooth-function state-preparation route of Holmes–Matsuura, has exact Hermite–Bernstein/tensor-train structure. The logical bound is \(G\le48n_p(2k+6)^3\), hence \(O(n_p)\) for fixed \(k\), with \(O(\log k)\) workspace under the stated exact-real contracts. This is not a complete finite-bit algorithm certificate: classical core generation, arithmetic and gate synthesis for
SP-HERMITE-POLY-002still need separate certification. Read the worked case and its scope → - Robin boundary block encoding: a smaller certified primitive.
For the selected \(n=3\) Robin boundary instance in Guseynov–Huang–Liu, Block encoding by signal processing, ASPBE reduced the audited \(T^{\dagger 3}\) branch from 49 to 30 \(T^{\dagger 3}\) gates and from 52 to 32 CNOTs, with the same five qubits and zero ancillas under the fixed primitive model.
- ASPBE and QuantumComputinglib.
The two application tracks, local workspace, task builder, and contributor review path are presented in one site.
- Blueprint and Library Explorer.
One generated inventory now drives the checked Blueprint catalog and searchable declaration browser.
- Public testing preview.
The site exposed separate State Preparation and Block Encoding directions and the user task builder.
- Earliest repository record.
The initial commit and timestamped manifest begin the public, auditable project history. No earlier date is asserted without evidence.
Part I · State Preparation
Chapters 1–2 are shared foundations authored once and reused by Block Encoding; Chapters 3–4 specialize them to preparation certificates.
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.
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.
Part II · Block Encoding
Block Encoding reuses the same finite-matrix and circuit nodes, then adds projected-block, composition, resource and proof-gated construction obligations.
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.
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.
Part III · Quantum Information and Representation Theory
PlannedLeditzky's representation-theoretic QIT notes organize one shared state/channel foundation followed by symmetry, Schur–Weyl and information-theoretic applications.
Explore planned chapters (not local certificates)
PlanStates, density operators and measurementsChoose one canonical finite-dimensional state, positive-operator, Born-rule and POVM layer before importing downstream results.PlanComposite systems, partial trace and purificationFreeze subsystem order and tensor conventions; purification and dilation remain non-unique representative constructions.PlanChannels, Choi maps, distances and operational testsCompletely positive maps, Kraus/Choi representations, trace/fidelity conventions and contractivity become shared nodes.PlanFinite-group and unitary representation foundationsGroup actions, representations, characters, averaging and fixed spaces are admitted only after manuscript-specific namespaces are purified.PlanYoung diagrams, Specht modules and Schur–Weyl dualityBuild the symmetric-group/unitary-group bridge needed by the quantum method of types; advanced Saxl and Foulkes–Howe results remain extensions, not prerequisites.PlanInvariant states, de Finetti, cloning and spectrum estimationConsume the shared QIT and representation layers without turning conceptual symmetry correspondences into Lean dependencies.PlanCapacity, entanglement, secret key and gamesAmplitude-damping capacity, entangled games and dimension-ten zero-key constructions are source routes above canonical state/channel adapters.PlanExtended chapter: quantum optics and channel counterexamplesPhoton-number entropy, PPT-square phenomena and explicit channel geometry are advanced consumers, not foundational definitions.
Part IV · Quantum Algorithms for Scientific Computation
PlannedLin–Wiebe's scientific-computing progression reuses Part II Block Encoding and adds transforms, simulation, estimation and application contracts.
Explore planned chapters (not local certificates)
PlanProbability, channels, query models, perturbation and statisticsShare QIT states/channels/distances and make query construction, precision and readout costs explicit.PlanBlock encoding as the shared scientific-computing interfacePoint back to Part II and add adapters only where the source notation or error convention differs.PlanAmplification, qubitization, QSP and QSVTSeparate polynomial/signal-transform correctness from phase synthesis and finite-gate compilation.PlanHamiltonian simulation and dynamicsCompose access, block/qubitization suppliers, approximation and successful execution under one resource tier.PlanFourier transforms, phase estimation and amplitude estimationUse the Comparator-backed exact Fourier route as an external resource theorem after circuit-model adaptation; it does not itself certify QPE.PlanEigenvalue and ground-state algorithmsCharge trial-state preparation, overlap, gap, precision, amplification and final classical output.PlanLinear systems, differential equations and open systemsReuse block/channel nodes and expose input, condition-number, success and readout assumptions rather than hiding them in an oracle.PlanExtended chapter: compilers, synthesis and circuit lower boundsExact factoring, shallow-circuit parity and oracle-assisted unitary synthesis extend the computing curriculum without counting as SP/BE successes.PlanExtended chapter: many-body model targetsThe Comparator-backed Laughlin route is a model-side spectral target and reusable mathematical substrate, not evidence of a quantum algorithm or simulator.