Moa Johansson

Researcher at Chalmers University

I'm interested in neuro-symbolic AI: the combination between neural networks and symbolic methods from logic and programming. The research of my group covers a wide range of applications ranging from language models for analyzing natural language for social science research, to formal methods and AI for mathematics and reasoning, and cognitive modeling. 

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.

←Back