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.
Figures & tables
Figure 1: The picture-frame (introduced by L’Huilier) is topologically the same as the torus, but not the icosahedron, which has no hole. In modern language, the symbols denote homeomorphisms , a precise notion of topological equivalence.
Figure 2: Summary of the Conjecturing agent. At each timestep, it picks its priors and chooses the number of features, then runs the first round of regression. This produces atomic formulae over patches of data, each governed by λi . In the second round of regression, these are combined by the scaffolder into a global statement. The variables and operators used are tailored to the application; a successful instance of learning is shown in the box on the right, with the heights and widths corresponding to the dimensions of vector spaces. Once in the environment, the statement gets translated into Lean. Quantifiers are implicitly added during the translation; the regression only has the variables and propositional symbols in its vocabulary. The Conjecturing agent cannot access the Lean statement. For further details, see §Appendix 5 .
Figure 3: Summary of the full system. The Conjecturing agent produces statements until one crosses the provability threshold whilst passing simple checks, at which point the episode terminates and it receives its greatest reward. At intermediate steps, it receives a smaller reward for longer statements, measured in terms of tree size. The Skeptical agent modifies the data distribution. The colour blue is used for the agents and the flow of information, whilst green is used for elements that are in the environment. Orange represents components that should be tailored to an application. Although the game is competitive, it is not zero-sum.
Figure 4Figure 5
Appendix figures & tables1 asset
Supplementary material from the paper’s appendix.
Appendix
Figure 6: In Subfigure I, the header code defines V0 , V1 and V2 as R -modules over a division ring R , and ∂i s (represented via D1 and D2 ) as R -linear maps. p1 - p4 are the rank-nullities, orientability and connectedness premises. The workflow in Subfigure II shows the translation in action for statement (1) over dataset D2 , picking out just p1 and p2 , the rank-nullities. Step 3 shows the two provers we tried: on the left, Lean Copilot’s search_proof , and on the right, the pre-written proof using grind and ring , tactics that are suited to algebra. In our experiments we saw no qualitative difference between these provers.
We study autonomous mathematical discovery in the Station, an open-world multi-agent environment in which AI agents from different model families pursue a shared research goal without a central coordinator or scripted pipeline. Agents choose their own research directions, conduct experiments, collaborate and publish papers. These papers accumulate into a shared body of knowledge that later agents can read, cite and extend. We evaluated the Station on 12 mathematical construction problems from the AlphaEvolve study and two additional case studies. Five of the 12 problems yielded results novel relative to the prior literature: a new infinite family of finite field Kakeya sets, new exact 604-point kissing configurations in eleven dimensions, improved bounds for the discretized Kakeya needle and sign uncertainty problems, and a substantially improved lower bound for Erdős's minimum overlap problem. Agents also discovered novel infinite families for Book Ramsey numbers. Their research extended beyond searching for high-scoring constructions: agents developed explanations of their findings and proved theorems outside the assigned tasks. These explanations guided further discoveries and were preserved in the agents' papers, making the underlying insights easier for external researchers to understand and build upon. All presented discoveries are supported by exact constructions or proofs formally verified in Lean. We release the source code, full agent dialogues, papers and verification code, providing a transparent record of how these discoveries emerged.
Stephen Chung, Wenyu Du, William J. Wesley
DualverseAI · University of Cambridge · University of Hong Kong +1
Mathematical communities work with different objects, invariants, and tools, so transferring a problem across them is expensive and often skipped. We present EULER, a multi-agent system that takes such a transfer--a bridge--as its unit of search. Around a fixed conjecture, EULER runs direct, adjacent-domain, and distant-domain routes in competition; a bridge keeps its budget only if it supplies an operation the source representation cannot execute and its target-side evidence returns to the original statement along a checked implication. Six ordered stress tests reject invalid bridges before expensive search begins. We evaluate EULER on 120 recent conjectures. The conjectures were frozen before search and screened for contamination, and are drawn from public papers by authors who had recently published in the Journal of Combinatorial Theory, Series A, a leading journal in combinatorics. EULER produced 10 proofs and 3 refutations, plus 45 scoped partial results. Two mechanisms held up under ablation: bridge-specific stress tests cut incorrect conclusions from 9 to 3, and bridge material combined with a target-native operation yielded a positive interaction of +4.2 resolved tasks that neither factor produced alone. Domain distance did not reliably predict success; executable operation gain and valid return did.
Automatically constructing well-specified and valuable mathematical conjectures remains a central challenge in AI-assisted mathematical discovery. Many existing open problems and conjectures are often too broad, underspecified, or difficult to connect to plausible proof or refutation strategies. We view a mathematical mechanism as a structure or reasoning principle that connects the assumptions of a candidate problem to its target conclusion, such as an inequality, invariant, decomposition, or reduction to an intermediate claim. We present MECA (MEchanism-centered Conjecture Agent), a multi-agent framework that constructs conjectures by jointly developing candidate statements and their supporting mechanisms. Explorer agents propose mechanisms, test how they apply, and revise the candidate conjecture accordingly, while critic agents assess their mathematical validity and research value. Their feedback guides changes to the assumptions, scope, and conclusion. Through this process, MECA transforms broad research directions into precise conjectures with substantive mathematical support while retaining a clearly identified unresolved core. We evaluate MECA in two complementary settings. First, we compare it with a generate-and-revise baseline on reconstructing preselected target-paper conclusions from target-conditioned but article-blind source materials. Second, we construct 100 semi-open problems from literature-derived seeds and existing open problems and evaluate them through independent proof and refutation attempts by automated provers. Our results indicate that mechanism-centered refinement produces well-specified and research-worthy conjectures that remain challenging for current automated provers.
Wentao Long, Yunfei Zhang, Chenyi Li +1
Fudan University · Qingdao University · Peking University