Symbolic, neural and neuro-symbolic methods for lemma discovery in proof assistants

The idea of getting computers to automatically discover mathematical conjectures is about as old as AI itself. With the advent of Large Language Models in combination with Proof Assistants, perhaps the time is now ripe to develop systems that can both capture some mathematical intuitions while retaining formal guarantees of correctness.

I will introduce the area of theory exploration: summarizing methods for conjecture discovery in symbolic, neural, and neuro-symbolic AI-systems, contrasting the pros- and cons of each, and discuss some ongoing work in my group.