Early Career Scientist Seminar: Marco David, UC Berkeley

Talk Title: 100 Quantum Theorems: A Benchmark for Formalizing Physics Abstract: Machine-checked proofs are fast becoming the gold standard in mathematics, with interactive theorem provers like Lean powering everything from DeepMind's IMO medal to OpenAI's Navier–Stokes formalization—yet quantum theory remains largely untouched by these tools. In this talk, Marco David presents joint work with Jens Palsberg on a curated benchmark of 100 quantum theorems designed to gamify the formal verification of quantum theory and quantum computing. Host: Theophilus Human