Abstract:

A century ago, Hilbert called upon the mathematical community to explain how to extract concrete numerical content from abstract proofs involving transfinite methods. For instance, from a qualitative proof of the existence of a limit, we might hope to extract a quantitative bound on the rate of convergence. Proof assistants based on modern type theory offer the tantalizing prospect of facilitating such extraction by running formalized proofs as programs—adding value to mechanization beyond verified correctness and collaborative proof engineering. In the talk, we will explore a case study from commutative algebra on this kind of proof mining, obtained in joint work with Peter Schuster.

Abstract:

Recent advances in generative models and reinforcement learning have enabled automatic theorem proving beyond the capabilities of classical methods. Scaling up data, model size, and inference compute has undeniably allowed us to prove more theorems. But is scaling alone enough to solve mathematical theorem proving? If not, what essential components might still be missing?

Abstract:

The advent of artificial intelligence raises an important question: Can AI assist mathematicians in solving open problems in mathematics? This talk explores this question from multiple perspectives. We will explore how different types of AI models can be trained to provide valuable insights into mathematical questions to recent progresses in the field of automated theorem proving.