This program is still work in progress.
Monday, January 6
9:3010:15 
Reid Barton: TBA 
10:1511:00 
Cyril Cohen: TBA 
11:0011:30 
coffee break 
11:3012:15 
Manuel Eberl: Automating Asymptotics in a Theorem Prover 
12:151:00 
Sébastien Gouëzel: On a Mathematician's Attempts to Formalize his Own Research in Proof Assistants

1:002:30 
lunch 
2:303:15 
Sicun Gao: Numerical Proofs in Nonlinear Control 
3:154:00 
Eva Darulova: Towards an Optimizing Compiler for Numerical Kernels 
4:004:30 
coffee break 
4:305:15 
Ulrik Buchholtz: TBA 
Tuesday, January 7
9:3010:15 
Neil Strickland: TBA 
10:1511:00 
Wenda Li: Reasoning with Nonlinear Formulas in Isabelle/HOL 
11:0011:30 
coffee break 
11:3012:15 
Fabian Immler: TBA 
12:151:00 
Patrick Massot: Formalizing a Sophisticated Definition 
1:002:30 
lunch

2:303:15 
Sylvie Boldo: A Coq Formalization of Lebesgue Integration of Nonnegative Functions 
3:154:00 
Geir Dullerud: TBA 
4:004:30 
coffee break 
4:305:15 
Markus Rabe: Deep Learning for Theorem Proving 
Wednesday, January 8
9:3010:15 
TBA 
10:1511:00 
Chantal Keller: SMTCoq: Coq Automation and its Application to Formal Mathematics 
11:0011:30 
coffee break 
11:3012:15 
Marijn Heule: Formal Methods and the Chromatic Number of the Plane 
12:151:00 
Gabriel Ebner: TBA 
Thursday, January 9
9:3010:15 
Sebastian Ullrich: TBA 
10:1511:00 
Discussion of Lean 4 
11:0011:30 
coffee break 
11:301:00 
Discussion: ongoing mathlib projects 
1:002:30 
lunch

2:304:00 
Contributed talks / discussion 
4:004:30 
coffee break 
4:305:15 
Mario Carneiro: TBA 
Friday, January 10
9:3011:00 
Contributed talks / discussion 
11:0011:30 
coffee break 
11:301:00 
Discussion: Lean tactics and tooling 
1:002:00 
lunch

2:002:30 
Peter Koepke: ForTheL as a Controlled Natural Language for Lean 
2:304:00 
Formal Abstracts 
4:30 
Kevin Buzzard colloquium at the University of Pittsburgh 