Textbook / teaching anchor
Quantum Computation and Quantum Information
Standard textbook reference for quantum mechanics, qubits, gates, and the circuit model.
Reading mode
Start visually; reveal formalism only when you want it.
Beginner layer · what the agent system actually does
The harness proposes; Lean decides what becomes library memory
An LLM can generate a plausible construction quickly. ASPBE separates that creative step from verification: failed routes are remembered, accepted routes carry exact proof roots, and only then are they exposed as reusable memory.
candidate
idea
reviewLeanmemory
certified route
- GenerateUpper agents propose decompositions or candidate circuits.
- CheckExecutable backends reject obvious circuit mistakes early.
- ProveLean discharges the exact semantic obligations.
- RememberOnly proof-backed constructions enter positive reusable memory.
Textbook / teaching anchor
Lecture Notes on Quantum Algorithms for Scientific Computation
Scientific-computing route from quantum preliminaries to block encoding, QSP, and QSVT.
Strict mathematics, after the picture
The equations behind the intuition
\[\text{generate}\rightarrow\text{check}\rightarrow\text{repair}\rightarrow\text{certify}\rightarrow\text{reuse}\]
Every symbol used here is connected below to a compiled declaration or a clearly marked research-source formula.
Textbook / teaching anchor
Quantum Computation and Quantum Information
Standard textbook reference for quantum mechanics, qubits, gates, and the circuit model.
Textbook / teaching anchor
Lecture Notes on Quantum Algorithms for Scientific Computation
Scientific-computing route from quantum preliminaries to block encoding, QSP, and QSVT.
Learn Lean while learning quantum computing
Lean idea: acceptance is a typed state transition
threeLayerCanonicalTrace_reachesAcceptedThe controller trace can reach `accepted` only through the reviewer stage with a recorded passing Lean gate.
The full proof-backed declarations for this chapter are shown immediately below.
System and evidence · Chapter 9 of 9
Search control, evidence, and open work
Show how typed stages, agent layers, candidate populations, proof gates, and explicit open problems coordinate without overstating evidence.
Lean modules used in this chapter
QuantumBlockEncoding/Automation.leanQuantumBlockEncoding/AutomationTrace.leanQuantumBlockEncoding/Literature.leanQuantumBlockEncoding/OpenProblems.leanQuantumBlockEncoding/OpenProblemsAudit.lean
Textbook lesson
Build the idea before opening the proof
ASPBE treats proof search as a controlled scientific process: freeze the contract, retrieve memory, test distinct routes, and promote only verified evidence.
Decompose before scaling
\[\text{goal}\rightarrow\text{proof DAG}\rightarrow\text{ready leaves}.\]
Parallel agents are added only when there are independent ready obligations or meaningfully different construction families.
Feedback changes the next action
\[\text{counterexample}\Rightarrow\text{retire parent route}.\]
Repeated identical failures do not justify more budget. The middle layer records the obstruction, updates the population, and chooses a new route or an adjacent tolerance tier.
Status is evidence
\[\text{Compiled}\ne\text{paper-wide complete}.\]
The site reports local compilation and broader route completion independently. CI regenerates counts and rejects proof holes.
Check your understanding
For any roadmap item, locate its declaration, its current evidence, and the one missing step before assigning another agent.
Mathematical order and conventions adapted from Lin, Lecture Notes on Quantum Algorithms for Scientific Computation. The formal checkpoints and ASPBE status distinctions are specific to this library.
Route at a glance
Where these results sit
flowchart LR
C["Candidate construction<br/>U"] --> F["Finite screen<br/>dimensions · unitarity · clean block"]
F --> L{"Named Lean theorem"}
L -- "closed" --> V["Certified construction"]
V --> E["Optional Qiskit /<br/>OpenQASM export"]
L -- "open" --> O["Explicit obstruction<br/>or missing proof leaf"]
O --> R["Change construction route<br/>or one declared ε rung"]
R --> C
classDef math fill:#ffffff,stroke:#5b6670,color:#222222,stroke-width:1.25px;
classDef proof fill:#ffffff,stroke:#2f7355,color:#18382b,stroke-width:1.6px;
classDef fail fill:#ffffff,stroke:#8a5a4a,color:#4c332c,stroke-width:1.4px;
class C,F,R math;
class L,V,E proof;
class O fail;
Selected declarations
Read the mathematics beside the Lean statement
A compiled route means that the reusable theorem or constructor and at least one finite witness compile. Hardware- and problem-specific downstream instantiations are out of scope, not universal claims made by these cards.
Lean result
Three-layer agent contracts
QuantumBlockEncoding.threeLayerAgentContracts
DeclarationCompiled
Full routeCompiled
\[\text{upper}\rightarrow\text{middle}\rightarrow\text{lower}\rightarrow\text{reviewer}\rightarrow\text{accepted}.\]
What it says
The harness records distinct responsibilities and a typed, executable handoff state machine for planning, refinement, proof work, and review.
Why it matters
Every handoff must be logged and carry an artifact; acceptance additionally requires both the Lean gate and reviewer approval. Hard tasks need explicit ownership and machine-checkable promotion conditions instead of repeated untracked prompts.
How the proof goes
Encode role contracts as data, define an executable transition guard, and prove that the canonical trace reaches acceptance while a failed Lean gate cannot do so.
- Uses
QuantumBlockEncoding.AutomationStage;QuantumBlockEncoding.AutomationTask;QuantumBlockEncoding.ThreeLayerTrace- Still outside this result
- None within the typed handoff and acceptance route. Running external models remains engineering evidence rather than a Lean theorem.
Route closure
QuantumBlockEncoding.threeLayerCanonicalTrace_allValidQuantumBlockEncoding.threeLayerCanonicalTrace_reachesAcceptedQuantumBlockEncoding.threeLayerAccepted_requiresLeanGateQuantumBlockEncoding.threeLayerAccepted_requiresReviewerApprovalQuantumBlockEncoding.threeLayerFailedGateTrace_notAccepted
Natural-language steps and Lean objects
| Mathematical step | Lean object or step |
|---|---|
| Declare stage and task types. | AutomationStage / AutomationTask |
| Instantiate layer contracts. | threeLayerAgentContracts |
| Check every typed handoff. | threeLayerCanonicalTrace_allValid |
| Require Lean and reviewer approval. | threeLayerAccepted_requiresLeanGate |
Open the Lean statement and source links
def threeLayerAgentContracts : List AgentContract :=
[
{
role := AgentRole.upper,
responsibility := "Fix the operator target, choose candidate families or proof leaves, compress trial memory, and reject weak directions.",
writes := ["runs/<run-id>/10_upper_director.md", "runs/<run-id>/90_handoff.md"],
mustLogTrial := true
},
{
role := AgentRole.middle,
responsibility := "Maintain the operator/candidate Lean--Markdown--LaTeX conversion window and proof-obligation ledger.",Local declaration · Verso Blueprint · commit-pinned GitHub source
Lean result
Open problems are first-class data
QuantumBlockEncoding.openProblems
DeclarationCompiled
Full routeCompiled
\[\mathcal O=[o_1,\ldots,o_7],\qquad \operatorname{Nodup}(\operatorname{id}(\mathcal O)).\]
What it says
Unfinished mathematical or engineering routes are listed explicitly with stable identifiers, status, evidence requirements, and source references.
Why it matters
A planned result cannot be mistaken for a theorem merely because it appears near compiled code. The registry route is itself audited even though the mathematical problems it contains intentionally remain open.
How the proof goes
Publish the typed records, prove that their identifiers are unique, and check that every entry has a nonempty statement, acceptance test, and reference list.
- Uses
QuantumBlockEncoding.OpenProblem;QuantumBlockEncoding.openProblemIds- Still outside this result
- The registry route is closed; its seven mathematical problems remain intentionally open and are not presented as solved theorems.
Route closure
QuantumBlockEncoding.openProblems_countQuantumBlockEncoding.openProblemIds_nodupQuantumBlockEncoding.openProblems_all_actionableQuantumBlockEncoding.openProblemRegistry_compiled
Natural-language steps and Lean objects
| Mathematical step | Lean object or step |
|---|---|
| Describe each obligation. | OpenProblem |
| Publish the current list. | openProblems |
| Check stable unique identifiers. | openProblemIds_nodup |
| Check actionable evidence fields. | openProblems_all_actionable |
Open the Lean statement and source links
def openProblems : List OpenProblem :=
[
{
id := "QBE-001",
title := "Gate-level Robin derivative block encoding for arbitrary stencil",
status := ProblemStatus.open,
statement := "Given a finite-difference stencil and Robin boundary data, synthesize the bulk-plus-boundary circuit for D and prove its block-encoding normalization.",
acceptanceTest := "A Lean VerifiedBlockEncoding whose concrete matrix semantics equal the requested derivative matrix and whose resource bound is O(kappa*n) plus coefficient-oracle cost.",
references := ["Guseynov-Huang-Liu 2025, one-term Robin theorem"]
},
{Local declaration · Verso Blueprint · commit-pinned GitHub source