–
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)
Video
–
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)
Video
–
Computer-Assisted Intuition: SAT Solvers in Mathematical Discovery

Bernardo Subercaseaux (CMU)
Video
–
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)
Video
–
Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification

Kaiyu Yang (Meta)
Video
–
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)
Video
–
Testing Artificial Mathematical Intelligence

Emily Riehl (Johns Hopkins University)
Video
–
Break
–
Proof Assistants for Logic, Computability, and Complexity

Yannick Forster (INRIA)
Video
–
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)
Video
–
Lean for the Research Mathematician (Virtual Talk)

Sophie Morel (ENS de Lyon)
Video
–
Break
–
Tool Demos/Exploration
–
Lunch (on your own)
–
Discussion
–
Break
–
Tool Demos/Exploration