This program is still work in progress.

Monday, January 6

9:30-10:15	Reid Barton: TBA
10:15-11:00	Cyril Cohen: TBA
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: TBA

Tuesday, January 7

9:30-10:15	Neil Strickland: TBA
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: TBA
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: TBA
4:00-4:30	coffee break
4:30-5:15	Markus Rabe: Deep Learning for Theorem Proving

Wednesday, January 8

9:30-10:15	TBA
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: TBA

Thursday, January 9

9:30-10:15	Sebastian Ullrich: TBA
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-4:00	Contributed talks / discussion
4:00-4:30	coffee break
4:30-5:15	Mario Carneiro: TBA

Friday, January 10

9:30-11:00	Contributed talks / discussion
11:00-11:30	coffee break
11:30-1:00	Discussion: Lean tactics and tooling
1:00-2:00	lunch
2:00-2:30	Peter Koepke: ForTheL as a Controlled Natural Language for Lean
2:30-4:00	Formal Abstracts
4:30	Kevin Buzzard colloquium at the University of Pittsburgh