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 |
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 |
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 |
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 |
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 |