QED. The Quest to Formalize Physics.

Abstract: Today’s gold standard for establishing new theoretical results in mathematics is an accompanying formal computer-verification of the theorems and their proofs. Interactive theorem provers (ITPs)—originally designed to verify computer algorithms—are now gaining significant traction in mathematical research. Systems such as Isabelle, Coq, and Lean provide programming languages that mechanize reasoning and thereby allow the verification of proofs. In 2024, Google DeepMind used reinforcement learning in such a formal language to win a silver medal at the International Mathematics Olympiad for the first time.

The potential of formal methods in quantum theory remains under-explored. In this talk, I will introduce a provocatively titled list of the “top 100” quantum theorems, aimed at gamifying and popularizing the formal verification of quantum theory. Building such a quantum library will provide a unified, searchable and cross-linked database of formalized mathematical knowledge. This can also allow training artificial intelligence models in an environment where precise details matter.

https://marcodavid.net/top100/