Computational mathematics in computer assisted proofs
September 12 to September 16, 2022
American Institute of Mathematics,
San Jose, California
and Svetlana Jitomirskaya
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:
- New computational tools/algorithms. Pure mathematics may need new
and different algorithms compared to the standard ones known in the
computational mathematics literature.
- 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?
- 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.
- 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
Material from the workshop
A list of participants.
A report on the workshop activities.
A list of open problems.