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

Program

Abstracts below.

A link to the recordings of the talks

https://www.youtube.com/@SorinBangu (external link)

Note that we weren't able to livestream or record the Q&A sections of the conference. Also, one talk (Michael Friedman's) wasn't livestreamed or recorded. 

Day 1: Wednesday 7^th October

9:00-9:15 Welcome by Sorin, Ásgeir, and Fenner

9:15-10:30 KEYNOTE Ursula Martin (Oxford, Edinburgh) The Leiden Declaration on AI and mathematics: roots, reception and reflection.

11:00-11:45 Fenner Tanswell (TU Berlin) On Autoformalisation

11:45-12:30 Markus Pantsar (RWTH Achen) Trust in mathematical AI systems

12:30-14:00 Lunch

14:00-14:45 Carolin Antos (Konstanz) Notions of (AI)-proofs

14:45-15:30 Michael Friedman (Bonn) Anxiety and Opacity: From AI-generated Proofs to Autoformalization

16:00-16:45 David Appadourai (Rome) Bidirectionality and the Epistemic Limits of Machine-Verified Proof

17:00-18:15 KEYNOTE Kati Kish Bar On (Boston Univ. and Harvard Business School, AI Institute) Rethinking Mathematical Intuition, Agency, and Practice in the Age of AI

Day 2: Thursday 8^th October

9:15-10:30 KEYNOTE Emily Riehl (Johns Hopkins Univ., Baltimore) A new paradigm for mathematical proof?

11:00-11:45 Silvia De Toffoli (IUSS Pavia) After Math

11:45-12:30 Ásgeir Berg (Iceland) Mathematical Understanding in the Time of Astra

12:30-14:00 Lunch

14:00-14:45 José Pérez-Escobar (Madrid) LLMs and rule-following in mathematics

14:45-15:30 Romain Büchi (Geneva) Conjecturing with AI: A View from Mathematical Practice

16:00-16:45 Sorin Bangu (Bergen) Rule-following and Rule-breaking: How is Mathematical Creativity Possible (in the Age of AI)

17:00-18:15 KEYNOTE Michael Harris (Columbia Univ., NYC) Purity as organizing principle

ABSTRACTS

• David Appadourai (Rome) Bidirectionality and the Epistemic Limits of Machine-Verified Proof

Neural theorem provers are measured by pass rate: the fraction of statements a kernel accepts a proof for. I argue that this leaves the decisive epistemic property unmeasured. A tactic script is bidirectional when a Lean-literate reader can reconstruct from the script alone the argument's case structure, its key lemmas and its strategy. The property belongs to the artifact and has a structural floor: below move-level inscription no reader reconstructs anything, whatever her competence. A kernel-accepted but unidirectional script yields instrument-warranted truth, not shareable proof. An audit of 805 machine proofs finds the two axes dissociating: 19.6% against 51.6%.

• Carolin Antos-Kuby (Konstanz) Notions of (AI)-proof

Are AI “proofs" actually proofs? In this talk, I will investigate different version of AI “proofs", such as output generated from LLMs, results by theorem provers and near-symbolic AI models. I test these against the so-called Standard Notion of Proof (SNP) show that SNP accepts AI-results as proof according to the same standards as human generated ones. This leads to undesirable consequences for the relation between proof and justification. I therefore propose a variant of SNP that highlights the role the right conceptual context plays in proving and argue that this resolves the problem of justification.

• Sorin Bangu (Bergen) Rule-following and Rule-breaking: How is Mathematical Creativity Possible (in the Age of AI)

Few notions are more important and yet less understood than mathematical creativity. In this talk, I aim to take some steps toward articulating a philosophical model helping us make better sense of the creative aspect of mathematics. The model builds on Margaret Boden's distinction between combinatorial and transformational creativity (Boden 2004; 2014), and integrates Feyerabendian insights about his so called 'epistemological anarchism', as well as the 'paradox' of rule-following (that Kripke claimed to find in Wittgenstein's Philosophical Investigations). However, I propose somewhat different accounts of both the combinatorial and the transformational kinds of creativity, where these modifications are suggested by reflections on several episodes in the history of mathematics. Importantly, the model doesn't presuppose (nor entails) that creativity is an exclusively human ability, so it allows us to consider the possibility, and hope, that AI systems (the current LLMs or of other type) could, and will, find creative solutions to outstanding mathematical problems. I shall argue that although the model doesn't a priori rule out this possibility, and hope, it also gives us a sense of how we should recalibrate such expectations.

• Asgeir Berg (Iceland) Mathematical Understanding in the Time of Astra

In this talk, I consider what effects the widespread use of AI in mathematical practice might have on our ability to understand mathematics. I argue that if more and more mathematical work were handed over to machines, mathematical practice would come under several distinct pressures that together would erode our collective ability to fully grasp what the machines produce, even when that work is done in collaboration with mathematicians, and, in the worst case, our ability to understand already established human mathematics.

• Romain Buechi (Geneva) Conjecturing with AI: A View from Mathematical Practice

This talk follows a concrete case of AI-assisted mathematical research, drawing out at each step its implications for an account of conjecturing and AI’s potential roles in it. The discussion examines how problem formulation, exploration, and proof interact, and how different participants and tools contribute to the advancement, support, and revision of conjectures. Throughout, I distinguish plausibility, pursuit worthiness, and fruitfulness, attending to the methods, connections, and mathematical understanding that an investigation yields. These reflections provide a basis for assessing AI’s different contributions to conjecturing beyond the generation of candidate statements, asking how it might help mathematicians select and shape fruitful lines of inquiry and judge their promise.

• Silvia De Toffoli (IUSS Pavia) After Math (joint work with Eamon Duede)

OpenAI’s announcement of an AI-generated solution to the Navier–Stokes problem has intensified speculation that mathematics might soon be “solved,” as many have said that chess and Go have been “solved.” In this talk, I challenge this narrative by questioning two assumptions on which it rests: that AI has genuinely solved a mathematical problem, and that mathematics is fundamentally about solving problems. In short, I will suggest that mathematical solutions require intelligible proofs that advance human understanding and that mathematics itself is a human enterprise that encompasses far more than problem solving. Recent AI achievements should not be thought of as a “human defeat.” Rather, they invite us to reconsider what mathematics is and what norms we should endorse to foster the flourishing of human mathematics.

• Michael Friedman (Bonn) Anxiety and Opacity: From AI-generated Proofs to Autoformalization

Recent AI-based mathematical developments cause various emotional reactions; Patrick Massot described an auto-formalization project as a scenario in which “AI companies […] [will] turn it [mathematics] in a giant radioactive wasteland”. Given such reactions, I examine both historically and contemporary discourses, how AI-generated proofs and autoformalisation transform mathematicians’ self-understanding, arguing that the dominant affect is not fear but rather anxiety, rooted in epistemic and structural opacity as well as in role-inversion. While in earlier decades calculating machines were largely intelligible, AI-based technologies are opaque, and moreover prompt uncoupling between proof production and its ‘digestion’. Anxiety hence emerges due to a destabilizing encounter with a non‑human agent that seems to know ‘too much’ and to socially shift the discipline itself.

• Michael Harris (Columbia Univ., Mathematics Dept.) Purity as organizing principle

Peter Sarnak has proposed an AlphaZero test, whose name is inspired by the DeepMind system that trained itself to evolve into the world go champion, as a way to determine whether or not mechanization of mathematics has any limits.  The test concerns a famous conjecture of Ramanujan, solved by Deligne in the early 1970s using methods entirely alien to and removed by several radical steps from Ramanujan's original formulation, based on his solution to the last of the Weil conjectures, also known as Deligne's purity theorem.  I will present the conjecture's successive reinterpretations as a case study for philosophers who hope to identify conditions that characterize how mathematical understanding survives the evolution of mathematical concepts.

• Kati Kish Bar On (Boston University & Harvard Business School, AI Institute) Rethinking Mathematical Intuition, Agency, and Practice in the Age of AI

The integration of artificial intelligence (AI) into mathematical practice raises profound questions about the nature of mathematical intuition in discovery and research. In this lecture, I examine the epistemological shifts induced by AI-based programs and tools, and explore how they challenge traditional notions of intuition, understanding, and mathematical agency. We argue that AI-based systems do not abolish intuition but relocate it, shifting it from a primarily anticipatory capacity to one that can also operate retroactively as interpretation, reconstruction, critique, and integration. Drawing on the historical flexibility of the concept, we propose a working definition of mathematical intuition as a family of practice-embedded capacities for orienting, evaluating, and rendering intelligible mathematical moves and outcomes across hybrid human–machine collaborations. Ultimately, we argue that AI-based programs, even when their capacities are more limited than some narratives suggest, are not merely new computational aids but a transformative epistemic force that reconfigures what it means to “do mathematics” in the 21st century.

• Ursula Martin (Oxford, Edinburgh. Mathematics Dept.) “A fragile and precious heritage”: mathematics research in the age of machines.

The use of AI in contemporary mathematical research is currently the subject of exuberant claims, and of significant external investment on a scale dwarfing more traditional government funding. Some extraordinary results are being achieved, especially with the use of mathematically enhanced LLMs, and many see tremendous potential for further impact. Some practitioners are convinced AI will be transformative; some are sceptical; and many are apparently unaware of the debate.

We frame the present moment by looking at how computation emerged very early as a tool for research in pure mathematics, making major and indispensable contributions to the twentieth century mathematical challenge of classifying finite simple groups.  Some of the first non-numeric computation on early machines, such as work of Max Newman, involved studying groups which could be represented as binary strings.  Initially researcher access was limited to scarce government funded machines, with terse papers stating results but giving little hint of how they were obtained.  Later, some leaders in the field advocated for the importance of mathematicians’ hands-on involvement in developing and maintaining algorithms and code, to ensure transparency, reproducibility and sustainability of the software effort. These teams pioneered the development of what we would now call open source software, early recognising the need for models of governance, reward and recognition for those so engaged.

While some were opposed to this democratisation, this model of infrastructure has become increasingly important in mathematics research with systems such as GAP and Sage released under the GNU public license and widely used around the globe.

With the advent of opaque black-box modern AI systems questions of transparency, reproducibility, sustainability have a new salience, yet it is unclear if the mathematical community would have the capacity to sustain production and governance of an open-source alternative.

• Markus Pantsar (Aachen) Trust in mathematical AI systems

AI systems are increasingly proficient in mathematics, from to now also solving research-level problems. This talk examines what trust in such systems requires. Comparing purely LLM-based systems to hybrid models using the rule-based prover Lean, I argue that robustness—performing reliably across circumstances—is key to trustworthy AI reasoning. But formal robustness is not the only issue. AI-generated and autoformalised proofs can be accepted, but if they are too long or complex for humans to read, what is their epistemic status? I consider what this means for assessing AI outputs, the future of mathematical review, and the mathematics profession itself.

• Jose Perez-Escobar (Madrid) LLMs and rule-following in mathematics

Large language models (LLMs) are increasingly used in mathematical research, raising questions about their role in mathematical practice. From a later Wittgensteinian perspective, mathematics can be understood as a rule-following practice whose stability depends not only on rules themselves, but on regularities in their communal application. This raises a problem for LLMs, which can reproduce such regularities without following rules in the same sense as humans, and may deviate from communal standards particularly in novel cases. However, human mathematical practice itself involves disagreement and open-ended rule extension. I argue that LLMs may become mathematical participants through their integration into these practices, potentially reshaping mathematical norms and regularities.

• Emily Riehl (Johns Hopkins Univ., Mathematics) A new paradigm for mathematical proof?

Mathematical proofs, whether human- or AI-generated, are getting longer and more complicated, which makes it much harder to verify that they are correct. This talk will explore a new paradigm for mathematical proof --- formal verification in a computer proof assistant --- and examine its effects on rigor, communication, and understanding. Anticipating a crisis in mathematical publishing accelerated by AI, we also ask how mathematical proofs should be communicated to present and future generations of mathematicians.

• Fenner Stanley Tanswell (TU Berlin) On Autoformalisation

At the start of September, Anthropic announced an autoformalisation of Fermat’s Last Theorem, taking up about 13.4 million lines of Lean code. Soon, it may be that large swathes of maths are autoformalised and checked for correctness. What will this do to fundamental mathematical concepts like proof, rigour, justification, and certainty? I will look at how well existing discussions of formalisation and proof can be applied to this new version of the question, as well as how the corporate source of the models entangles our philosophical questions with political, environmental, and ethical ones.