Machine Assisted Proofs

February 13 - 17, 2023

Schedule

All times in this Schedule are Pacific Time (PT)

Monday, February 13, 2023

Morning Session
8:00 - 8:55 Check-In/Breakfast (Hosted by IPAM)
8:55 - 9:00 Welcome & Opening Remarks: Dean Miguel García-Garibay (Dean of Physical Sciences, UCLA) and Dima Shlyakhtenko (Director, IPAM)

Session Chair: Terence Tao (University of California, Los Angeles)
9:00 - 9:50
Adam Topaz (University of Alberta)

Liquid Tensor Experiment

10:00 - 10:15 Break
10:15 - 11:05
Benedikt Ahrens (Delft University of Technology)

Univalent Foundations and the UniMath library

11:15 - 11:30 Break
11:30 - 12:20
Andrej Bauer (University of Ljubljana)

Formalizing invisible mathematics
PDF Presentation
12:30 - 2:30 Lunch (on your own)

Afternoon Session

Session Chair: Jeremy Avigad (Carnegie Mellon University)
2:30 - 3:20
3:30 - 4:00 Break
4:00 - 4:50
5:00 - 5:30 Junior Participant Intros Part I
5:30 - 6:45 Reception (Location: IPAM Lobby)

Tuesday, February 14, 2023

Morning Session
8:00 - 9:00 Check-In/Breakfast (Hosted by IPAM)

Session Chair: Emily Riehl (Johns Hopkins University)
9:00 - 9:50
10:00 - 10:15 Break
10:15 - 11:05
11:15 - 11:30 Break
11:30 - 12:20
Adam Wagner (Worcester Polytechnic Institute)

Finding counterexamples to conjectures via reinforcement learning
PDF Presentation
12:30 - 2:30 Lunch (on your own)

Afternoon Session

Session Chair: Marc Lackenby (University of Oxford)
2:30 - 3:20
Haniel Barbosa (Universidade Federal de Minas Gerais in Belo Horizonte)

Better SMT proofs for certifying compliance and correctness
PDF Presentation
3:30 - 4:00 Break
4:00 - 4:50
Anne Baanen (Vrije Universiteit)

Computing with or despite the computer
PDF Presentation

Wednesday, February 15, 2023

Morning Session
8:00 - 9:00 Check-In/Breakfast (Hosted by IPAM)

Session Chair: Akshay Venkatesh (Institute for Advanced Study)
9:00 - 9:50
10:00 - 10:15 Break
10:15 - 11:05
Assia Mahboubi (Institut National de Recherche en Informatique Automatique (INRIA))

Verifying computational mathematics
PDF Presentation
11:15 - 11:30 Break
11:30 - 12:20
12:30 - 12:40 Group Photo - MAP2023
12:40 - 2:30 Lunch (on your own)

Afternoon Session

Session Chair: Jordan Ellenberg (University of Wisconsin-Madison)
2:30 - 3:20
3:30 - 4:00 Break
4:00 - 4:50 Panel - “Prospects in machine assisted proof” (Sophie Morel, Emily Riehl, Akshay Venkatesh)
5:00 - 5:30 Junior Participant Intros Part II

Thursday, February 16, 2023

Morning Session
8:00 - 9:00 Check-In/Breakfast (Hosted by IPAM)

Session Chair: Assia Mahboubi (Institut National de Recherche en Informatique Automatique)
9:00 - 9:50
10:00 - 10:15 Break
10:15 - 11:05
Pascal Fontaine (Université de Liège)

SMT: quantifiers, and future prospects
PDF Presentation
11:15 - 11:30 Break
11:30 - 12:20
James Davenport (University of Bath)

How to prove a calculation correct?
PDF Presentation
12:30 - 2:30 Lunch (on your own)

Afternoon Session

Session Chair: Geordie Williamson (University of Sydney)
2:30 - 3:20
Maria Ines de Frutos Fernandez (Imperial College London)

Formalizing Norm Extensions and Applications to Number Theory
PDF Presentation
3:30 - 4:00 Break
4:00 - 4:50

Friday, February 17, 2023

Morning Session
8:00 - 9:00 Check-In/Breakfast (Hosted by IPAM)

Session Chair: James Davenport (University of Bath)
9:00 - 9:50
Petra Hozzova (Technische Universität Wien)

Automation of Induction in Saturation
PDF Presentation
10:00 - 10:15 Break
10:15 - 11:05
11:15 - 11:30 Break
11:30 - 12:20
Heather Macbeth (Fordham University at Lincoln Center)

Algorithm and abstraction in formal mathematics
PDF Presentation