Formal Methods in Mathematics /
Lean Together 2020

Monday, January 6
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
Tuesday, January 7
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
Wednesday, January 8
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
Thursday, January 9
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
Friday, January 10
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