Progress and Roadmap

Local proof completion is not route completion

Counts below are generated from the declaration inventory. Milestones are curated against the actual modules and openly name partial, experimental, planned, and blocked work.

1,886Compiled route labels

537Partial route route labels

0Stated, proof incomplete route labels

395Experimental route labels

4Planned route labels

0Blocked route labels

flowchart LR
  C["Compiled<br/>core contracts"] --> E["Compiled<br/>BE Case 1 and 2"]
  E --> P["Partial route<br/>amplitude oracle"]
  P --> Q["Planned<br/>concrete QSVT"]
  E --> X["Experimental<br/>paper backend"]
  X --> B["Blocked<br/>historical raw fold"]
  B --> F["Finite semantic bridge<br/>and projection proof"]

Milestone	Broader route status
State-preparation contracts and first-column consumer	Compiled
Textbook Pauli X and Hadamard certificates	Compiled
Circuit syntax to matrix semantics	Compiled
Reusable exact block-encoding routes	Compiled
Finite three-bit primitive banded sparse access	Compiled
BE Case 1 transfer-operator certificate	Compiled
BE Case 2 exact Householder certificate	Compiled
Finite two-qubit cubic primitive amplitude oracle	Compiled
Degree-one QSVT identity consumer realization	Compiled
Three-layer controller trace and registry audit	Compiled
Fixed-N8 Robin T3 reproduction and evolved winner	Compiled
Arbitrary-width banded-access source resource compiler	Planned
General QSVT phase synthesis and approximation checker	Planned
GHL Theorem 4 A-to-H Hamiltonian composition	Compiled
Arbitrary-width GHL one-term primitive resource compiler	Planned
Historical Robin H-free raw-fold rejection	Compiled

Paper reproduction queue

What has been reproduced, and what has not

This table is generated from the Lean-compiled literature registry. A compiled local lemma does not promote a paper-wide route unless its circuit, oracle, projection, normalization, and resource obligations are all closed.

Status	Paper	Role	Target and next step
Compiled	Quantum framework for simulating linear PDEs with Robin boundary conditions Nikita Guseynov, Xiajie Huang, Nana Liu (2026)	`primaryTarget`	`QuantumBlockEncoding/GHLHamiltonian.lean` Fixed-N8 one-term source circuits are primitive-certified; Theorem 4 A/A-dagger to S1,S2 to H source LCU composition is formalized with an explicit Eq. (30) phase audit and phase-balanced S1 correction. Arbitrary-width primitive resource compilation remains a separate frontier.
Partial route	Efficient explicit gate construction of block-encoding for Hamiltonians needed for simulating partial differential equations Nikita Guseynov, Xiajie Huang, Nana Liu (2025)	`explicitBlockEncoding`	`QuantumBlockEncoding/BandedSparseAccess.lean` Periodic-boundary predecessor and baseline for derivative/operator encodings.
Partial route	Asymptotically Optimal Quantum Circuits for Comparators and Incrementers Vivien Vandaele (2026)	`arithmeticCircuits`	`QuantumBlockEncoding/PromiseGateOptimization.lean` ASPBE formalizes the controlled-conjugation and involutory dirty-flag identities; the paper's complete comparator and incrementer constructions remain outside current scope.
Planned	Explicit block encodings of boundary value problems for many-body elliptic operators Tyler Kharazi, Ahmad M. Alkadri, Jin-Peng Liu, Kranthi K. Mandadapu, K. Birgitta Whaley (2025)	`explicitBlockEncoding`	`QuantumBlockEncoding/OpenProblems.lean` Explicit circuits for elliptic operators and Dirichlet, Neumann, Robin boundaries.
Planned	Explicit quantum circuits for block encodings of certain sparse matrices Daan Camps, Lin Lin, Roel Van Beeumen, Chao Yang (2024)	`explicitBlockEncoding`	`QuantumBlockEncoding/Circuit.lean` Sparse-matrix block encoding circuits; important comparison point for generated circuits.
Planned	FABLE: Fast Approximate Quantum Circuits for Block-Encodings Daan Camps, Roel Van Beeumen (2022)	`explicitBlockEncoding`	`QuantumBlockEncoding/Circuit.lean` Approximate direct circuit synthesis for dense or structured matrices.
Planned	On efficient quantum block encoding of pseudo-differential operators Haoya Li, Hongkang Ni, Lexing Ying (2023)	`explicitBlockEncoding`	`QuantumBlockEncoding/OpenProblems.lean` Dense operator family; useful for variable-coefficient PDE operators.
Planned	Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics Andras Gilyen, Yuan Su, Guang Hao Low, Nathan Wiebe (2019)	`qsvtFramework`	`QuantumBlockEncoding/BlockEncoding.lean` Core block-encoding and QSVT framework.
Planned	Optimal Hamiltonian simulation by quantum signal processing Guang Hao Low, Isaac L. Chuang (2017)	`qsvtFramework`	`QuantumBlockEncoding/OpenProblems.lean` Hamiltonian simulation primitive used after a block encoding is available.
Planned	Hamiltonian simulation using linear combinations of unitary operations Andrew M. Childs, Nathan Wiebe (2012)	`qsvtFramework`	`QuantumBlockEncoding/BlockEncoding.lean` LCU composition is central to combining block encodings.
Planned	Exponential improvement in precision for simulating sparse Hamiltonians Dominic W. Berry, Andrew M. Childs, Richard Cleve, Robin Kothari, Rolando D. Somma (2014)	`qsvtFramework`	`QuantumBlockEncoding/Resources.lean` Sparse Hamiltonian simulation and query-model baseline.
Planned	Quantum simulation of partial differential equations via Schrodingerization Shi Jin, Nana Liu, Yue Yu (2024)	`pdeSimulation`	`QuantumBlockEncoding/OpenProblems.lean` Transforms non-unitary PDE dynamics into Hamiltonian simulation tasks.
Planned	Quantum circuits for partial differential equations via Schrodingerisation Junpeng Hu, Shi Jin, Nana Liu, Lei Zhang (2024)	`pdeSimulation`	`QuantumBlockEncoding/OpenProblems.lean` Circuit-level PDE simulation reference around Schrodingerisation.
Planned	Efficient explicit circuit for quantum state preparation of piece-wise continuous functions Nikita Guseynov, Nana Liu (2024)	`statePreparation`	`QuantumBlockEncoding/OpenProblems.lean` Amplitude oracle ingredient for coefficient functions.
Planned	Multivariable quantum signal processing (M-QSP): prophecies of the two-headed oracle Zane M. Rossi, Isaac L. Chuang (2022)	`qsvtFramework`	`QuantumBlockEncoding/OpenProblems.lean` Boundary of current multivariate polynomial transformation techniques.
Planned	A logarithmic-depth quantum carry-lookahead adder Thomas G. Draper, Samuel A. Kutin, Eric M. Rains, Krysta M. Svore (2004)	`arithmeticCircuits`	`QuantumBlockEncoding/Circuit.lean` Arithmetic subroutine source for explicit oracle implementations.
Planned	Optimizing quantum circuits for arithmetic Thomas Haener, Martin Roetteler, Krysta M. Svore (2018)	`arithmeticCircuits`	`QuantumBlockEncoding/Circuit.lean` Arithmetic circuit optimization relevant to gate-level oracle costs.

Planned longitudinal experiment

Does a larger certified memory actually help?

Each newly reproduced paper adds memory cards only after its named Lean roots compile. Earlier cold and warm benchmarks are then replayed in fresh, isolated worktrees with the same model, prompt budget, target, tolerance ladder, and acceptance gates. We compare solve rate, accepted-cycle count, token proxy, wall time, and invalid-route count. Historical run artifacts are never injected into the cold arm.