Formal Methods in Mathematics /
Lean Together 2020

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