Computational mathematics in computer assisted proofs

Computational mathematics in computer assisted proofs

This workshop, sponsored by AIM and the NSF, 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.

This event will be run as an AIM-style workshop. Participants will be invited to suggest open problems and questions before the workshop begins, and these will be posted on the workshop website. These include specific problems on which there is hope of making some progress during the workshop, as well as more ambitious problems which may influence the future activity of the field. Lectures at the workshop will be focused on familiarizing the participants with the background material leading up to specific problems, and the schedule will include discussion and parallel working sessions.

The deadline to apply for support to participate in this workshop has passed.

For more information email workshops@aimath.org

Plain text announcement or brief announcement.