Computational mathematics in computer assisted proofs

September 12 to September 16, 2022

at the

American Institute of Mathematics, San Jose, California

organized by

Charles Fefferman, Anders Hansen, and Svetlana Jitomirskaya

Original Announcement

This workshop will be devoted to the use of computational mathematics in computer assisted proofs.

There are an increasing number of famous conjectures and theorems that have recently been proven using computer assisted proofs. A highly incomplete list in alphabetical order includes the Dirac-Schwinger conjecture, the double bubble conjecture, Kepler's conjecture (Hilbert's 18th problem), Smale's 14th problem, the 290-theorem, the weak Goldbach conjecture etc. In many of these cases the proofs are based on using numerical computations with approximations, a technique that belongs to the field of computational mathematics and scientific computing rather than computer science.

Numerical approximations used in computer assisted proofs may be an incredibly powerful tool for pure mathematicians and such tools may change the way we approach many problems in mathematics. The workshop aims to explore the full potential of computational mathematics in computer assisted proofs by bringing pure and computational mathematicians together, focusing on the following:

  1. New computational tools/algorithms. Pure mathematics may need new and different algorithms compared to the standard ones known in the computational mathematics literature.
  2. Which computational problems can or cannot be used in computer assisted proofs? Not all computational problems can be computed with a 100% certain output. For example, feasibility of linear programs can be decided given rational entries, however, that is not always the case with irrational inputs. This begs the question: which computational problems are safe to use?
  3. Software for easy use in practical theorem proving. Standard software in scientific computing may not be sufficient for theorem proving because of the lack of rigorous guarantees on the output. Thus, software packages for the pure mathematician are needed.
  4. Reproducibility of computer assisted proofs. Both computer hardware and software are subject to becoming out-of-date. Hence, the reproducibility of results for future generations becomes a serious issue.

Material from the workshop

A list of participants.

A report on the workshop activities.

A list of open problems.

Workshop Videos