Mathematical Proof in the Age of AI: Conceptual Implications of the Use of Artificial Intelligence in Mathematical Research

This conference will be about the conceptual-philosophical implications of AI-based proving and autoformalisation for mathematics. Examples include the resolution of various Erdos problems by Google DeepMind’s Alethia model, the recent disproof of the unit distance conjecture by OpenAI’s GPT model, and the (partial) autoformalisations of sphere packing in dimension 8 and 24 by the model Gauss from Math Inc. 

We aim to reflect on how these technologies may transform mathematical practice, with a concentration on the practice of creating and verifying proofs. While some view the use of LLMs, and AI in general, as heralding a new era of machine-assisted mathematics, others caution against overestimating their capabilities and warn of the downsides of automating mathematics. The workshop aims to critically assess the role of AI-based mathematics, striking a balance between optimism and scepticism.

The conference will be livestreamed, recorded, and made available online (with speakers’ permission).