Keynote: AI for Mathematical Discovery: Symbolic, Neural and Neuro-Symbolic Methods - Moa Johansson |Lambda Days 25

[CodeSync]

Keynote: AI for Mathematical Discovery: (…) Neuro-Symbolic Methods - Moa Johansson |Lambda Days 25

Keynote: AI for Mathematical Discovery: (...) Neuro-Symbolic Methods - Moa Johansson |Lambda Days 25

This talk was recorded at Lambda Days in June 2025. If you’re curious about our upcoming event, check https://lambdadays.org

Keynote: AI for Mathematical Discovery: Symbolic, Neural and Neuro-Symbolic Methods

Learning to construct new, interesting, and useful lemmas for reasoning about mathematics or computer programs in proof assistants is yet an underexplored area in AI. Proof assistants such as the Lean, Isabelle and Coq systems are increasingly being used also by research mathematicians to enable big collaborations and checking details of very large proofs. Fields medallist Terrence Tao has even famously said that he believes AI-enabled proof assistants will become trustworthy co-authors of mathematics as early as 2026.

However, formalising mathematics is still a time-consuming endeavour requiring expertise. Work in autoformalisation aims at translating mathematics expressed in English into the language of proof assistants, while in this talk, I will describe our work on the related task of conjecturing lemmas. The aim is to suggest lemmas that can aid a human user working on a mathematical formalization, as well as strengthen automated theorem provers.

We examine how LLMs can be used for lemma generation, and how they can be combined with symbolic tools for optimal results. Our aim is to provide a first tool towards generic conjecturing over a broad range of mathematical theories, which is practically useful for users of proof assistants.

Comments welcome! View the code-sync tag for more Code Sync talks!