Abstract: Interactive theorem verification is a powerful tool for mathematical research and software development, but so far the training and effort required have limited its use to critical software applications and a few flagship mathematical theorems such as the four color theorem and Hales' proof of the Kepler conjecture. But over the coming decade we predict that advances in AI will make ITV more accessible, and provide new tools such as semantic search for mathematical proofs, data and software. Thus it is timely to discuss how these tools could help the broader community of mathematical scientists, and begin to design systems to realize this potential.
We discuss this in the context of examples drawn from celestial mechanics, dynamical systems theory and computational biology. Our examples involve numerical integration of ordinary differential equations, but they also require formal and symbolic methods to derive the ODEs and analyze the results. We review recent work such as Immler’s verification of Tucker’s solution of Smale’s 14th problem, and extrapolate it to suggest ways that physicists, computational biologists and others could use AI enhanced ITV and search in their work.
