The Quantum Formalization Drive

Measuring a quantum system disturbs it. The information–disturbance tradeoff asks how little a measurement that yields a given amount of information about an unknown state must change that state. The question underlies the security analysis of quantum key distribution, where an eavesdropper's information gain is paid for in detectable disturbance, and the…

Quantum technologies usually prepare a desired state by isolating a system and driving it with carefully timed unitary operations; coupling to an environment is treated as noise. Dissipative state preparation reverses this view: one engineers the system–environment coupling so that the open-system dynamics itself drives every initial state into a prescribed…

Integrals of polynomial functions of the matrix entries of a random element of a compact group appear across mathematical physics and probability: in random matrix theory (moments of Haar-distributed unitary, orthogonal and symplectic matrices), in lattice gauge theory (the link integrals of $U(N)$ gauge fields), and in quantum information (averages of…

Classical Hamiltonian mechanics describes an observable by a function on a phase space. Its Poisson bracket gives observables a Lie algebra: the bracket is antisymmetric and satisfies the Jacobi identity. In multisymplectic geometry, a higher-degree differential form replaces the symplectic two-form, and the appropriate observables may themselves be…

Near-term quantum processors have few qubits, while the circuits one would like to run (variational eigensolvers, sampling benchmarks, error-mitigated algorithms) often need more qubits than any single device has. Peng, Harrow, Ozols and Wu (arXiv:1904.00102, Phys. Rev. Lett. 125, 150504, 2020) show that a circuit which is only loosely connected (a few…

We develop entanglement-of-formation potentials for feedback-assisted classical communication and one-way randomness distillation. For a finite-dimensional quantum channel without initial shared entanglement, an exact amortization theorem bounds the increase of message information plus entanglement remaining across the communicating laboratories. This…

This paper describes a formalization of discrete real closed fields in the Coq proof assistant. This abstract structure captures for instance the theory of real algebraic numbers, a decidable subset of real numbers with good algorithmic properties. The theory of real algebraic numbers and more generally of semi-algebraic varieties is at the core of a number…

A max-XORSAT instance asks for a binary assignment that satisfies as many parity constraints as possible. A matrix specifies the parity check in each constraint, while a second binary vector specifies the desired parity. The objective can be written as the number of satisfied constraints minus the number violated, so an assignment with a high objective…

Experiments that prepare many-body entangled states (GHZ, W, stabilizer, cluster and matrix product states) need a way to check that the device produced the intended state. Full quantum state tomography answers the question but its cost grows with the dimension $d = 2^n$ of an $n$-qubit system: a reconstruction needs on the order of $d^2$ measurement settings.…

Quantum search starts with a state that has some overlap with a desired target. Standard Grover iterations can increase that overlap quickly, but their success probability oscillates with the number of iterations. If the initial overlap is unknown, a sequence chosen for one value can pass the target and perform poorly at another. Earlier fixed-point…

Quantum computers need error correction, and the codes that are cheapest to run in hardware are quantum low-density parity-check (LDPC) codes: every check involves a bounded number of qubits, and every qubit takes part in a bounded number of checks. For a long time the only well-understood quantum LDPC codes were surface codes such as Kitaev's toric code,…

Determining an unknown quantum state of $n$ qubits to good accuracy requires, in general, a number of copies of the state exponential in $n$; this follows from Holevo's theorem. One way around this barrier is to restrict the class of states. Stabilizer states are the natural candidate: they are the states produced from $|0^n\rangle$ by Clifford circuits, they…

This mission develops Chapter 4 of Quantum algorithms for optimizers by Giacomo Nannicini. The chapter's selected results describe the mathematical guarantees below.

In the AdS/CFT correspondence a quantum theory of gravity in an asymptotically anti-de Sitter spacetime is equivalent to a conformal field theory on its boundary. A central question is how local bulk physics is encoded in the boundary theory, and in particular which bulk region is described by a given boundary subregion $R$. Harlow's TASI 2017 lectures (arXiv:…

Simulating the time evolution $e^{-iHt}$ of a many-body Hamiltonian is one of the main proposed uses of quantum computers. For a Hamiltonian $H = \sum_X h_X$ whose terms act on small, nearby groups of sites of a lattice, Haah, Hastings, Kothari and Low give a quantum algorithm whose gate count is nearly linear in the space-time volume $n t$, and show that this is…

In the usual textbook presentation, quantum theory starts from postulates that have no obvious operational meaning: states are density operators on a complex Hilbert space, measurements are positive operators, and probabilities are given by the trace formula $p=\mathrm{tr}(\hat A\hat\rho)$. In Quantum Theory From Five Reasonable Axioms (Hardy 2001), Lucien…

Quantum walks give quadratic speed-ups for a class of search problems that classical algorithms solve by running a Markov chain until it hits a marked state. Ambainis's element-distinctness algorithm (Ambainis 2007) and Szegedy's quantization of reversible Markov chains (Szegedy 2004) are the two starting points. Magniez, Nayak, Roland and Santha (arXiv:quan…

Parallel repetition is useful for amplifying errors in nonlocal games, but a joint entangled strategy can correlate outcomes across repetitions. Independence of the sampled questions does not imply independence of wins. The pinned manuscript supplies the research context.

Positive partial transpose imposes strong constraints on quantum maps, but composition may retain entanglement. Explicit finite-dimensional examples make that distinction a precise algebraic target. The pinned manuscript supplies the research context.