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.

Abstract:

Automated reasoning tools such as constraint solvers, finite model builders and theorem provers could be very useful for mathematicians. I will give a brief introduction to these tools and their possible applications to research mathematics. I will also try to understand why few mathematicians use them in their day-to-day work and give some suggestions for increasing uptake as a topic for discussion in the workshop.

Abstract:

I’ll critically examine where I think generative AI could replace me—as in, which parts of my work might be (better) carried out by a neural network than me. I’ll start with presenting a small project I’ve been working on with Michael Rawson to train a neural network to generate Agda proof terms, which sets the scene for what I think AI will be most helpful with. I’ll then sketch two research projects I’ve been working on, one on proof automation in cubical type theory and one at the intersection of linear logic and dependent type theory, and will try to gauge where AI could have helped my work, and which parts of the projects really required me to bang my head against the wall in a sustained fashion.