–
Coffee and Check-In
–
Welcome remarks from Simons and SLMath
–
The Carleson Project: Collaboration Using Formalization
Floris van Doorn (University of Bonn)
–
Machine Learning for Algorithm Design
Maria-Florina Balcan (Carnegie Mellon University)
–
Break
–
Lean Tutorial
–
Lunch (on your own)
–
Remarks by Patrick Shafto about a new DARPA program on AI & Math
–
Lean Tutorial/Exercises
–
Break
–
Lean Tutorial/Exercises
–
Coffee and Check-In
–
Solving Semidecidable Problems in Group Theory
Giles Gardam (University of Bonn)
–
Computer-Assisted Intuition: SAT Solvers in Mathematical Discovery
Bernardo Subercaseaux (CMU)
–
Break
–
Machine Learning Tutorial
–
Lunch (on your own)
–
Machine Learning/Exercises
–
Break
–
Machine Learning/Exercises
–
Reception at SL Math
–
Coffee and Check-In
–
How can Machine Learning Help Mathematicians?
Amaury Hayat (Ecole des Ponts - Institut Polytechnique de Paris)
–
Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification
Kaiyu Yang (Meta)
–
Break
–
SAT Tutorial
–
Lunch (on your own)
–
SAT Tutorial / Exercises
–
Break
–
SAT Tutorial / Exercises
–
Coffee and Check-In
–
Adventures with an Automatic Prover
Jeffrey Shallit (University of Waterloo)
–
Testing Artificial Mathematical Intelligence
Emily Riehl (Johns Hopkins University)
–
Break
–
Proof Assistants for Logic, Computability, and Complexity
Yannick Forster (INRIA)
–
Lunch (on your own)
–
Tool Demos/Exploration
–
Break
–
Tool Demos/Exploration
–
Coffee and Check-In
–
Challenges in State-of-the-Art Bit-Precise Reasoning
Aina Niemetz (Stanford University)
–
Lean for the Research Mathematician (Virtual Talk)
Sophie Morel (ENS de Lyon)
–
Break
–
Tool Demos/Exploration
–
Lunch (on your own)
–
Discussion
–
Break
–
Tool Demos/Exploration