Automated Reasoning, Formal Proof Assistants & Frontier Research Mathematics
Simons Institute for the Theory of Computing
32:30·2026·graduate level·Research Seminar
UC Berkeley Simons Institute session examining formal verification (Lean), neuro-symbolic theorem proving, and where frontier mathematical discovery differs from contest benchmarks.
In the latest episode of our Polylogues web series, Simons Institute Director Venkat Guruswami interviews Dan Spielman (Yale) and Nikhil Srivastava (Simons Institute), two of the organizers of First Proof, a project that aims to measure the capabilities of AI systems in the context of research mathematics. First Proof announced its forthcoming benchmark and second batch of problems this past weekend, on Pi Day 2026.
Comments
Add a comment...Sign in