Discovering mathematical concepts through a multi-agent system
Daattavya Aggarwal, Oisin Kim, Carl Henrik Ek, Challenger Mishra
cs.AI
Mar 4, 2026 · v2
math.HO
TL;DR
Conjectures are translated into Lean 4 theorems over Mathlib linear algebra and proved with Lean Copilot or grind/ring, giving proof feedback to the agents.
Abstract
Mathematical concepts emerge through an interplay of processes, including experimentation, efforts at proof, and counterexamples. In this paper, we present a new multi-agent model for computational mathematical discovery based on this observation. Our system, conceived with research in mind, poses its own conjectures and then attempts to prove them, making decisions informed by this feedback and an evolving data distribution. Inspired by the history of Euler's conjecture for polyhedra and an open challenge in the literature, we benchmark with the task of autonomously recovering the concept of homology from polyhedral data and knowledge of linear algebra. Our system completes this learning problem. Most importantly, the experiments are ablations, statistically testing the value of the complete dynamic and controlling for experimental setup. They support our main claim: that the optimisation of the right combination of local processes can lead to surprisingly well-aligned notions of mathematical interestingness.
Problem
AI systems for mathematics mostly solve problems that are already posed. It is unclear whether they can autonomously form interesting concepts and conjectures. The paper tests whether a system can rediscover homology, meaning the Betti numbers and their relation to the Euler characteristic, from polyhedral data and linear algebra knowledge.
Approach
A multi-agent system has a Conjecturing agent that proposes symbolic statements by regression over data on polyhedra (spheres, tori, Klein bottles, disjoint unions), given as incidence matrices. Each statement is translated by handcrafted code into a Lean 4 theorem, with Mathlib-style modules and linear maps as boilerplate and premises such as rank-nullity as hypotheses. A prover (Lean Copilot's search_proof, or a fixed proof using grind and ring) returns a binary proof score. That score shapes the conjecture distribution and the evolving data distribution.
Results
The full system recovered statements equivalent to relations between the Euler characteristic and the Betti numbers. Ablations, including a regression-only trial, did not produce these concepts, which supports the value of the combined conjecture-proof dynamic. The two provers showed no qualitative difference.
