Skip to content

doc(roadmap): drop landed BQP ⊆ PP and narrow feasible interpolation to what remains #1965

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 1 commit into from
Oct 31, 2026
Merged

doc(roadmap): drop landed BQP ⊆ PP and narrow feasible interpolation to what remains #1965

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 6 additions & 5 deletions ROADMAP.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -338,10 +338,10 @@ DLOGTIME-uniform AC⁰ under explicit conventions.

- Proof-space lower bounds, Frege, cutting planes, polynomial calculus and sum-of-squares, and
certified DPLL solver runtimes.
- **Feasible interpolation:** from a Resolution refutation of `A(x,y) ∧ B(x,z)`, construct a
circuit separating the `x` assignments extendible to `A` from those extendible to `B`, with
proof-size and extraction-time bounds. Prove the monotone variant under its polarity
hypotheses and transfer circuit and communication lower bounds to proof-size lower bounds.
- **Feasible interpolation** ([#1817]): extraction-time bounds for Resolution interpolants over
an explicit circuit encoding; a sharper monotone separator bound (Alon–Boppana) for a
stronger clique–coloring size lower bound; and the transfer of communication lower bounds to
proof-size lower bounds.
- **Proof search:** automatizability and weak automatizability with explicit encodings and
runtime dependence on the shortest proof; proof-search reductions built on the Cook–Reckhow
and p-simulation APIs; then reflection principles and bounded-arithmetic witnessing theorems.
Expand Down Expand Up @@ -455,7 +455,7 @@ each statement against the numbered result. Organize modules by subject, not cha
`Kolmogorov/Conditional.lean`, and `Kolmogorov/MINcKT.lean`), as independently scoped
developments; the reverse
multi-tape-to-single-tape simulation and machine-backed Nisan–Wigderson decoding.
- **Quantum computation** ([#896]): BQP ⊆ PP; reusable
- **Quantum computation** ([#896]): reusable
circuit, channel and measurement semantics with uniformity and approximation costs, reusing
suitable quantum foundations rather than incompatible models; BQP, QMA and related query,
communication and interactive classes, with amplification, containments and complete
Expand Down Expand Up @@ -868,5 +868,6 @@ not planned, not as proved.
[#1449]: https://github.com/cslib-community/complexitylib/issues/1449
[#1524]: https://github.com/cslib-community/complexitylib/issues/1524
[#1572]: https://github.com/cslib-community/complexitylib/issues/1572
[#1817]: https://github.com/cslib-community/complexitylib/issues/1817
[#1819]: https://github.com/cslib-community/complexitylib/issues/1819
[#1824]: https://github.com/cslib-community/complexitylib/issues/1824
Loading