Abstract

Mathematics is humanity’s most infinite frontier, and formalising and discovering new theorems has been painstakingly slow. Today, AI promises a paradigm shift. In this talk, I examine the technical breakthroughs AI brings to building an AI-human collaborative mathematician capable of genuine discovery. I discuss how human intuition and AI reasoning can work together to explore, conjecture, and solve mathematical problems. I then introduce AI methods that can extract informal human domain knowledge, formalise it, learn from it, tackle new problems, and rigorously verify solutions. I highlight how the scarcity of high-quality conjectures limits AI learning, and propose automated generation of progressively better conjectures to enhance AI reasoning. Ultimately, I argue that by centring the human in this partnership, we can build an AI-human mathematician that not only solves problems, but fundamentally expands how we explore and discover mathematics.