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.