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 |