Machine Assisted Proofs - IPAM

Machine Assisted Proofs

February 13 - 17, 2023

Schedule

All times in this Schedule are Pacific Time (PT)

Monday, February 13, 2023

Morning Session

08:00-08:55
Check-In/Breakfast (Hosted by IPAM)
08:55-09: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)
09:00-09: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

Afternoon Session

12:30-14:30
Lunch (on your own)
Session Chair: Jeremy Avigad (Carnegie Mellon University)
14:30-15:20
John Harrison (Amazon Web Services)
Virtual Talk: a personal and historical perspective
15:30-16:00
Break
16:00-16:50
Geordie Williamson (University of Sydney)
What can the working mathematician expect from deep learning?
17:00-17:30
Junior Participant Intros Part I
17:30-18:45
Reception (Location: IPAM Lobby)

Tuesday, February 14, 2023

Morning Session

08:00-09:00
Check-In/Breakfast (Hosted by IPAM)
Session Chair: Emily Riehl (Johns Hopkins University)
09:00-09:50
Marc Lackenby (University of Oxford)
Using machine learning to formulate mathematical conjectures
10:00-10:15
Break
10:15-11:05
Leonardo de Moura (Microsoft Research)
Virtual Talk: The Lean proof assistant: introduction and challenges
11:15-11:30
Break
11:30-12:20
Adam Wagner (Worcester Polytechnic Institute)
Finding counterexamples to conjectures via reinforcement learning

Afternoon Session

12:30-14:30
Lunch (on your own)
Session Chair: Marc Lackenby (University of Oxford)
14:30-15:20
Haniel Barbosa (Universidade Federal de Minas Gerais in Belo Horizonte)
Better SMT proofs for certifying compliance and correctness
15:30-16:00
Break
16:00-16:50
Anne Baanen (Vrije Universiteit)
Computing with or despite the computer

Wednesday, February 15, 2023

Morning Session

08:00-09:00
Check-In/Breakfast (Hosted by IPAM)
Session Chair: Akshay Venkatesh (Institute for Advanced Study)
09:00-09:50
Micaela Mayero (Galilee Institute - Paris Nord University)
Virtual Talk: An overview of the real numbers in theorem provers: an application with real analysis in Coq
10:00-10:15
Break
10:15-11:05
Assia Mahboubi (Institut National de Recherche en Informatique Automatique (INRIA))
Verifying computational mathematics
11:15-11:30
Break
11:30-12:20
Patrick Massot (Université Paris-Saclay)
Formal mathematics for mathematicians and mathematics students

Afternoon Session

12:30-12:40
Group Photo - MAP2023
12:40-14:30
Lunch (on your own)
Session Chair: Jordan Ellenberg (University of Wisconsin-Madison)
14:30-15:20
Tony Wu (Google)
Autoformalization with Large Language Models
15:30-16:00
Break
16:00-16:50
Panel - “Prospects in machine assisted proof” (Sophie Morel, Emily Riehl, Akshay Venkatesh)
17:00-17:30
Junior Participant Intros Part II

Thursday, February 16, 2023

Morning Session

08:00-09:00
Check-In/Breakfast (Hosted by IPAM)
Session Chair: Assia Mahboubi (Institut National de Recherche en Informatique Automatique)
09:00-09:50
Jason Rute (IBM)
Deep learning in interactive theorem proving
10:00-10:15
Break
10:15-11:05
Pascal Fontaine (Université de Liège)
SMT: quantifiers, and future prospects
11:15-11:30
Break
11:30-12:20
James Davenport (University of Bath)
How to prove a calculation correct?

Afternoon Session

12:30-14:30
Lunch (on your own)
Session Chair: Geordie Williamson (University of Sydney)
14:30-15:20
Maria Ines de Frutos Fernandez (Imperial College London)
Formalizing Norm Extensions and Applications to Number Theory
15:30-16:00
Break
16:00-16:50
Bohua Zhan (Chinese Academy of Sciences)
Virtual Talk: Verifying symbolic computation in the HolPy theorem prover
Printable Version