Every record is classified by how it was verified. The badge shows the strongest tier of evidence; the chips list each method that applies.
≡Exact & formal
The defining behavior was checked exactly: a mathematical identity, a full statevector or stabilizer simulation, or an exhaustive basis-state truth table.
Direct mathematics
An analytic identity or closed-form derivation proves the defining property (e.g. H² = I, Y = iXZ).
Unitary / matrix equivalence
The circuit's unitary was computed and compared against the reference matrix.
Exact statevector simulation
A full statevector simulation reproduced the exact expected state or distribution.
Reversible classical logic was checked exhaustively (or at edge cases) on computational-basis inputs.
✓Strong empirical
The design was verified by construction plus measured evidence: statistical re-execution, small-instance analytic agreement, sub-block, echo, or invariant checks. Scale-specific bugs can still survive.
Statistical re-execution
Measured counts from independent executions agreed within statistical tolerance (e.g. TVD bounds).
Small-instance agreement
The same generator matched analytic results at tractable sizes; large instances are inferred.
The circuit follows a specification whose correctness argument is standard; the construction was audited against it.
◐Attested & literature
The record rests on external authority: peer-reviewed papers, standard textbooks, expert review, or evidence carried over from related verified entries. Nothing here was re-executed by this catalog.
Peer-reviewed paper
The record's claims trace to one or more peer-reviewed publications cited on the entry.
Textbook / standard citation
The behavior is standard material (e.g. Nielsen & Chuang, OpenQASM spec) and is cross-referenced, not re-derived.
Expert review
A named human reviewer with domain expertise checked the record.
Tangential evidence
Correctness is supported indirectly through related verified entries (e.g. a gate verified inside a verified algorithm).
○Automated & unreviewed
Only automated (LLM-assisted) review or an unreviewed community submission backs this record so far. Treat it as a starting point, not evidence.
LLM-assisted review
An LLM checked the record for internal consistency. Useful screening, not evidence of correctness.
Community submission
Submitted by the community and not yet through the review pipeline.
15 public entries
Atlas stars stay in this public list. Saving an entry to your workspace starts an unstarred private copy.
Find a better parameterized ansatz for the quantum approximate optimization algorithm (QAOA) applied to combinatorial optimization problems such as Max-Cut, where the standard, fixed-form QAOA ansatz is not known to be optimal and no systematic method exists for improving on it.
Evaluate candidate designs for a simplified cooling system within an engineering design process that normally requires numerous computationally intensive numerical simulations, in a way that avoids the data input/output overhead that otherwise erodes any quantum speedup on such simulation tasks.
Given a set of constraints over a finite field, such as a max-XORSAT instance or the task of finding a degree-n polynomial over 𝔽ₚ that approximates a given data set as well as possible, produce an assignment that satisfies as many constraints as possible.
Given a hard combinatorial problem, rewrite it as an Ising spin model whose lowest-energy spin configurations are exactly that problem's solutions, so that a machine which minimizes energy can be pointed at the problem at all.
Given the low autocorrelation binary sequences (LABS) problem, an optimization problem that is classically intractable even for moderately sized instances, determine whether QAOA can act as an algorithmic component that provides an advantage over the best classical exact solvers.
Solve large-scale Maximum Cut (MaxCut) problems on near-term quantum hardware by decomposing the graph into many subgraph problems that can be solved in parallel, and determine how such a decomposition compares to a purely classical alternative for the same task.
Given a target position for a robot manipulator's end effector, find joint angles that reach it — the inverse kinematics problem, which has no analytical solution for a general 6-degree-of-freedom arm and admits many joint configurations at once for a redundant one.
Sample from the final limiting distribution πₙ of a slowly varying sequence of Markov chains, where πₙ is chosen to concentrate on good solutions of a combinatorial optimization problem.
Given a network's vulnerabilities and how their connectivity creates kill-chains — paths to security compromise — decide which vulnerabilities to prioritize for patching, so that those paths are removed.
Given a list of m + 1 Hermitian n × n matrices C, A_1, A_2, …, A_m and m numbers b_1, …, b_m, find the positive semidefinite n × n matrix X that maximizes tr(CX) subject to the constraints tr(A_j X) ≤ b_j for j = 1, 2, …, m, approximately, to within ± ε of the optimum. The Zoo states that semidefinite programming has many applications in operations research, combinatorial optimization, and quantum information, and that it includes linear programming as a special case. All three papers reduce that optimization to a feasibility question by binary search on a guess for the optimal value, but not to the same feasibility question, and the difference carries a parameter that the runtimes below then depend on. Brandão and Svore add the constraint tr(X) ≤ R, with R a measure of the size of the optimal solution, and test the dual: they sample from the distribution y divided by the 1-norm of y for a dual feasible vector y. Van Apeldoorn, Gilyén, Gribling and de Wolf likewise test membership in a dual polytope induced by the current primal candidate, with R bounding the trace of an optimal primal X. Brandão, Kalev, Li, Lin, Svore and Wu instead normalise the primal to tr(X) = 1 and test it directly, deciding whether the constraints tr(A_i X) ≤ a_i + ε admit a positive semidefinite X of unit trace; Chia, Gilyén, Li, Lin, Tang and Wang adopt that same trace-one form for the dequantized version.
Schedule a workflow of tasks — an instance of the workflow scheduling problem, a known NP-hard class of scheduling problems — for an industrial use case, in a way that can be represented and solved by quantum, classical, and hybrid quantum-classical algorithms.
Given oracle access to the m × n payoff matrix of a zero-sum game with bounded entries, compute a classical representation of an ε-approximate Nash equilibrium of that game.