What you can find here
Here, you can explore theorems and conjectures in mathematical physics, quantum information, quantum error correction and quantum computing. Each page brings together the statement, assumptions, source papers, available proofs and formalizations. We welcome suggestions for new entries, including questions for which no proof is yet known.
Our aim is to build a detailed, useful record of each result as research develops. This may include original and alternative proofs, proposed arguments, counterexamples and later progress, with clear references and credit to the people behind the work. Some entries already have extensive proof histories; others offer a starting point through statements and literature references.
We describe human and AI contributions according to the authors’ disclosures. Human-written, AI-assisted and AI-generated arguments are distinguished where the sources allow. Reviews and explanations are included to help readers understand and assess the arguments.
As new work appears, we aim to connect each question with established solutions, partial results, numerical evidence, proposed proofs and critiques. Dates and scope help readers see what has changed and what remains open.
For Lean formalizations, we provide links to repositories, theorem statements and project documentation, together with information about their scope and assumptions. We survey these resources without running external Lean code. “Not found in our survey” means we searched without finding a resource; “not surveyed” means we have not yet searched.
The collection currently contains 679 results and continues to grow.
Sources and open data
Visit Resources to explore the websites, problem collections and Lean projects we use, with credits to their authors, editors and contributors.