Top 100 Quantum Theorems

by Marco David and Jens Palsberg

This list collects 100 important theorems in quantum physics, quantum information and quantum computing. Inspired by the list of the top 100 mathematical theorems of which Freek Wiedijk tracks the formalization progress, this is a similarly arbitrary and necessarily incomplete list with no particular order.

We welcome submissions from your interactive theorem proving community, and will link formal proofs below.

Acknowledgements. Thank you to Rodolfo R. Soldati, Alex Meiburg, Serge Massar, Tein van der Lugt, Debbie Leung, Matilde Baroni, Eduardo Martín-Martínez, Jean-Yves Desaules, Maksym Serbyn for their contributions. We are grateful for support by the NSF Challenge Institute for Quantum Computation.

Legend:
Foundations Mathematical Physics Quantum Information Quantum Algorithms Condensed Matter High Energy Physics

The List

1. The Spectral Theorem   Isabelle: linkRocq: linkLean: link 1, link 2
2. Eigenstates in an infinite square well  
3. The Quantum Harmonic Oscillator  
4. Ehrenfest’s Theorem  
5. Quantum tunneling through a finite potential barrier  
6. Conservation of the probability (4-)current 
7. Eigenstates of a δ-distribution well 
8. Heisenberg Uncertainty Relation  
9. Baker–Campbell–Hausdorff Formula  
10. Trotter Product Formula (Lie–Trotter–Kato)  
11. Simultaneous diagonalization of commuting observables  
12. Noether’s Theorem  
13. Wigner’s Theorem  
14. Stone–von Neumann Theorem  
15. Spectrum of the hydrogen atom (Coulomb potential)  
16. Addition of angular momentum (e.g. Clebsch–Gordan)  
17. Wigner–Eckart Theorem  
18. Power-series spectrum of a perturbed time-independent Hamiltonian 
19. Dyson series for time-dependent perturbation theory  
20. Correctness of the Rayleigh–Ritz method  
21. Correctness of the Born–Oppenheimer approximation  
22. The Adiabatic Theorem  
23. Berry phase (Geometric phase)  
24. Superdense coding  
25. Quantum teleportation with shared entanglement  
26. No-Cloning Theorem / No-Broadcast Theorem / No-Teleportation Theorem  
27. No-Communication Theorem  
28. No-Deleting Theorem  
29. Schrödinger–HJW Theorem (purification of mixed states) 
30. Schmidt decomposition for Hilbert spaces  
31. Bell’s Theorem (QM violates CHSH inequality)  
32. Monogamy of entanglement  
33. Tsirelson bound  
34. Correctness of the Deutsch–Jozsa algorithm   Rocq: link
35. Correctness of Shor’s algorithm   Rocq: link
36. Correctness of Grover’s algorithm   Rocq: link
37. The Bennett–Bernstein–Brassard–Vazirani Theorem (BBBV)  
38. Quantum key distribution by BB84  
39. Impossibility of quantum bit commitment (Mayers–Lo–Chau) 
40. Solovay–Kitaev Theorem  
41. Universality of sets of two-qubit quantum gates  
42. Universality of the Toffoli and the Hadamard  
43. Five two-qubit gates are necessary and sufficient to implement a Toffoli gate 
44. Six two-qubit linear nearest-neighbor gates are necessary and sufficient to implement a Toffoli gate 
45. 3n CX gates are necessary to implement a multi-control Toffoli gate with n-1 controls 
46. Adiabatic and gate-based quantum computing are equivalent up to polynomial factors  
47. The Threshold Theorem (quantum fault-tolerance)  
48. Petz recovery map  
49. Choi’s Theorem on completely positive maps  
50. Choi–Jamiołkowski isomorphism (channel-state duality)  
51. Gelfand–Naimark–Segal construction  
52. Gelfand–Naimark Theorem  
53. Krein–Milman Theorem  
54. Stinespring’s Factorization Theorem / Naimark’s Dilation Theorem   Lean: link
55. Continuous Functional Calculus   Lean: link 1, link 2
56. Gleason’s Theorem  
57. Holevo’s Theorem  
58. Pusey–Barrett–Rudolph Theorem  
59. Kochen–Specker Theorem  
60. The Spectral Theorem for PVMs  
61. Strong subadditivity of quantum entropy  
62. Entanglement-assisted classical capacity of quantum channels  
63. Quantum state discrimination for two states (Ivanović–Dieks–Peres Limit)  
64. The Lloyd–Shor–Devetak Theorem for quantum channel capacity  
65. Eastin–Knill Theorem  
66. Gottesman–Knill Theorem  
67. Magic state distillation  
68. Correctness of distillation of Bell pairs 
69. 1D gapped Hamiltonians have area-law ground states 
70. The Lieb–Robinson bound  
71. Onsager’s solution to the 2D Ising model  
72. MIP* = RE 
73. BQP \(\subseteq\) PP  
74. QIP = PSPACE 
75. Quantum Stein Lemma 
76. Quantum 3-SAT is QMA1-complete 
77. Computing the Jones polynomial at roots of unity is BQP-hard 
78. Uniqueness of 4-dimensional representations of the Clifford algebra (up to unitary equivalence) 
79. Spin-statistics Theorem  
80. Reeh–Schlieder Theorem  
81. Wick’s Theorem  
82. Elitzur’s Theorem  
83. 2D TQFTs are equivalent to Frobenius algebras  
84. Chern–Simons theory can compute the Jones polynomial  
85. The CFT central charge is its entanglement entropy 
86. Osterwalder–Schrader Reconstruction Theorem  
87. 4D Gaussian free field theory satisfies the Osterwalder-Schrader axioms  Lean: link
88. Bisognano–Wichmann Theorem 
89. Wood–Spekkens–Bell Theorem 
90. Correctness of block encoding 
91. Correctness of Hamiltonian simulation by Trotterization 
92. Correctness of Hamiltonian simulation by Linear Combination of Unitaries 
93. Correctness of Hamiltonian simulation by Qubitization 
94. Qubit reuse is NP-complete 
95. Correctness of a quantum circuit optimizer  Rocq: link
96. Correctness of the toric code  
97. Correctness of entanglement-assisted stabilizer codes 
98. The Knill–Laflamme conditions 
99. Correctness of approximate circuit synthesis 
100. Correctness of Simon’s algorithm  Rocq: link

Honorable Mentions

• Mermin–Wagner Theorem
• Goldstone’s Theorem
• Proof of correctness of the Harrow–Hassidim–Lloyd (HHL) algorithm
• Oracle Separation of BQP and PH (Raz & Tal, STOC 2019)

Disclaimer: Any opinions, findings, and conclusions or recommendations expressed on this site are those of the authors and do not necessarily reflect the views of the National Science Foundation.