Abstract:
Computer assisted proofs have become increasingly popular over the last decades and turn out to be instrumental when proving many long standing conjectures. Striking examples are the computer assisted proof of Kepler’s conjecture (Hales et al) on optimal packing of 3-spheres, and the computer assisted proof of the of the Dirac-Schwinger conjecture (Fefferman and Seco) on the asymptotic behaviour of the ground-state energy of certain Schrodinger operators. What may be surprising is that the computational problems used in these proofs, and several others, are non-computable according to Turing. In this talk we will discuss this paradoxical phenomenon: Not only can non-computable problems be used in computer assisted proofs, they are crucial for proving important conjectures. A key tool for understanding this phenomenon is the Solvability Complexity Index (SCI) hierarchy, which allows for a classification theory for all types of computational problems. This classification theory is a key for pure mathematicians to determine which computational problems may be used in computer assisted proofs. In particular, there are non-computable problems that can be used and there are non-computable problems that are so difficult that they can never be used in computer assisted proofs. The question is: which ones are safe to utilise? The talk is aimed for a general mathematical audience, and examples from different areas of mathematics will be provided.
427 Thackeray Hall