Early Career Scientist Seminar: Marco David, UC Berkeley

Tuesday Oct 6, 2026, 2:00 PM → 3:00 PM US/Eastern

WLE 102 (Wright Laboratory)

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.