Machine Assisted Proofs

February 13 - 17, 2023

Overview

A number of core technologies in computer science are based on formal methods, that is, a body of methods and algorithms that are designed to act on formal languages and formal representations of knowledge. Such methods include interactive proof assistants, automated reasoning systems (including first-order theorem provers and satisfiability solvers), computer algebra systems, and knowledge representation and database systems. Methods based on machine learning have also led to the discovery of new mathematical results.

The goal of this workshop is to bring mathematicians and computer scientists together to explore potential applications of these technologies to the domain of pure mathematics, building upon the exciting recent developments in this subject.

The workshop aims to have equal representation from both the computer science and pure mathematics communities and to encourage constructive dialogue. On the computer science side, we intend to attract experts who have developed the technologies enumerated above and who have shown an interest in mathematical applications. On the mathematical side, we hope to attract researchers from a diversity of fields who are intrigued by the possibility of using the new technologies in their work and are open to exploration. The meeting will promote an exchange of ideas, and we hope to leave ample time for open-ended conversation and collaborative discussion.

Organizing Committee

Erika Abraham (RWTH Aachen University)
Jeremy Avigad (Carnegie Mellon University)
Kevin Buzzard (Imperial College)
Jordan Ellenberg (University of Wisconsin-Madison)
Tim Gowers (University of Cambridge)
Marijn Heule (Carnegie Mellon University)
Terence Tao (University of California, Los Angeles (UCLA))