| 9:30-10:15 | Reid Barton: Formalizing O-minimality |
| 10:15-11:00 | Cyril Cohen: Generating Mathematical Structure Hierarchies Using Coq-ELPI |
| 11:00-11:30 | coffee break |
| 11:30-12:15 | Manuel Eberl: Automating Asymptotics in a Theorem Prover |
| 12:15-1:00 | Sébastien Gouëzel: On a Mathematician's Attempts to Formalize his Own Research in Proof Assistants |
| 1:00-2:30 | lunch |
| 2:30-3:15 | Sicun Gao: Numerical Proofs in Nonlinear Control |
| 3:15-4:00 | Eva Darulova: Towards an Optimizing Compiler for Numerical Kernels |
| 4:00-4:30 | coffee break |
| 4:30-5:15 | Ulrik Buchholtz: Higher Algebra in Homotopy Type Theory |
| 9:30-10:15 | Neil Strickland: Using Lean for New Research |
| 10:15-11:00 | Wenda Li: Reasoning with Non-linear Formulas in Isabelle/HOL |
| 11:00-11:30 | coffee break |
| 11:30-12:15 | Fabian Immler: The Poincaré-Bendixson Theorem in Isabelle/HOL |
| 12:15-1:00 | Patrick Massot: Formalizing a Sophisticated Definition |
| 1:00-2:30 | lunch |
| 2:30-3:15 | Sylvie Boldo: A Coq Formalization of Lebesgue Integration of Nonnegative Functions |
| 3:15-4:00 | Geir Dullerud: Statistical Model Checking of Stochastic Hybrid Systems with Logic-Based Specifications |
| 4:00-4:30 | coffee break |
| 4:30-5:15 | Markus Rabe: Deep Learning for Theorem Proving |
| 9:30-10:15 | Alexei Lisitsa: First-Order Theorem (Dis)proving for Reachability Problems in Verification and Experimental Mathematics |
| 10:15-11:00 | Chantal Keller: SMTCoq: Coq Automation and its Application to Formal Mathematics |
| 11:00-11:30 | coffee break |
| 11:30-12:15 | Marijn Heule: Formal Methods and the Chromatic Number of the Plane |
| 12:15-1:00 | Gabriel Ebner: Integration of General-Purpose Automated Theorem Provers in Lean |
| 9:30-10:15 | Sebastian Ullrich: State of the ⋃ |
| 10:15-11:00 | Discussion of Lean 4 |
| 11:00-11:30 | coffee break |
| 11:30-1:00 | Discussion: ongoing mathlib projects |
| 1:00-2:30 | lunch |
| 2:30-3:00 | Koundinya Vajjha: A Formal Proof of PAC Learnability for Decision Stumps (contributed talk) |
| 3:00-4:00 | Contributed talks / discussion |
| 4:00-4:30 | coffee break |
| 4:30-5:15 | Mario Carneiro: Metamath Zero, or: How to Verify a Verifier |
| 9:30-10:00 | William Simmons: Polynomial Rings with Operators in Coq (contributed talk) |
| 10:00-10:30 | Peter Koepke: ForTheL as a Controlled Natural Language for Lean |
| 10:30-11:00 | Discussion |
| 11:00-11:30 | coffee break |
| 11:30-1:00 | Discussion: Lean tactics and tooling |
| 1:00-2:00 | lunch |
| 2:00-2:15 | Luis Berlioz: A Database of Definitions |
| 2:20-2:45 | Jesse Han: The Continuum Hypothesis |
| 2:45-3:15 | Floris van Doorn: Tactics |
| 3:15-4:00 | Thomas Hales: Controlled Natural Language |
| 4:30 | Kevin Buzzard colloquium at the University of Pittsburgh |