QuantumComputinglib × Math 2.0
A living knowledge network and a quality Lean library support our core mission: explain quantum constructions clearly and teach their reusable ideas.
ASPBE is the construction system; QuantumComputinglib is the library and teaching surface. State preparation and block encoding are the current focus.
In Terence Tao's Math 2.0 talk (Caltech, 2026), slides 18–21 put human understanding at the center of sustainable AI-assisted mathematics. Slides 22, 25 and 26 give nine examples of useful work. The map below is our interpretation of those examples, not an official nine-goal framework or an endorsement.
Our original goals of connected knowledge, reusable Lean proofs and clearer quantum teaching predate and resonate with this report. We invite collaborators in quantum algorithms, formalization, education and mathematical AI to improve the teaching and test what proof maps can reveal.
Foundations (2, 3) → understanding (1, 8) → research agenda (4, 5, 6, 7, 9). Existing infrastructure gives us a starting point; each next step still needs its own evidence.
Foundations
02 · Living knowledge networks
Existing: source-anchored paper maps, implementation records, a mechanism atlas and the shared Lean graph connect constructions and their obligations.
Next: update source and dependency records together so a changed assumption exposes every affected route.
Inspect the implementation map →03 · Quality formal libraries
Existing: shared finite-matrix, circuit, state-preparation and block-encoding interfaces have a generated declaration inventory and publication gates.
Next: close missing semantic adapters and proof obligations; extend the library through reviewed reusable declarations.
Browse the Lean library →Core value
01 · Open exposition problems
Existing: proof-digestion records and theorem-linked figures expose the registers, normalization, projection and resource model behind a circuit.
Next: compress repetitive bookkeeping into reusable conceptual moves, with lossless links back to assumptions and Lean. The Functor Hypergraph is a navigation lens; categorical correctness requires separate certificates.
Read the Robin construction map →08 · Interactive texts and presentations
Existing: the book map, worked cases, natural-language/Lean views and graph navigation offer several routes into the same mathematics.
Next: improve motivated reading paths and reader evaluation. Parts III–IV are source-anchored curricula with local certificates still pending.
Start with the reading guide →Research agenda
04 · Principles, methods and insights
Existing: the Hermite–Bernstein/tensor-train case and shared preparation/block-encoding graph expose structural connections.
Next: test whether a shared mechanism transfers to a new construction. A graph shortcut suggests a question; a checked bridge supplies evidence.
Explore the structured-state case →05 · Theorem-level ablation studies
Existing: source-blind encoder–denoiser review reconstructs meaning from Lean and audits hidden hypotheses. This is infrastructure for ablations.
Next: fix the same conclusion, remove a named theory or proof input, then supply another proof or a precise obstruction. Harness-route ablations measure a different question and do not establish this result.
Inspect the review workflow →06 · Theorem neighborhoods
Existing: exact/approximate contracts and explicit oracle, register, ancilla and normalization boundaries identify what may be varied.
Next: weaken a condition, trace affected graph edges, and check a generalization or a counterexample under a new sealed statement.
Explore the block-encoding contracts →07 · Interpretable open math models
Existing: concise Lean interfaces, natural-language counterparts, source links and typed failed routes can support explainable mathematical tools.
Next: curate training/evaluation packets from our own or appropriately licensed exposition/proof pairs and test semantic fidelity. External references are not automatically eligible model data. We do not claim a trained model or certified safety; visible explanations do not expose a model's private internal reasoning.
See the contribution packet →09 · Model failure and misalignment
Existing: the library separates ideal circuits, exact-real resource models, finite diagnostics, finite-bit synthesis and external application assumptions.
Next: expose boundary violations, misleading oracle costs and model hallucinations through explicit failure cases. A model-level counterexample or Lean proof alone does not certify real hardware reliability.
Read an explicit finite-bit boundary →