Automated Conjecturing: Generation, Selection, and Evaluation

Deciding which conjectures are worth proving is a crucial part of mathematical discovery, and a system that learns mathematics from its axioms alone must make that decision without human guidance. Self-play provers such as Minimo learn a conjecturer alongside the prover and reward it for producing hard conjectures, but a conjecture that is harder to prove is not necessarily more useful for improving a prover: the learned conjecturer drifts toward long, artificial statements. We study conjecturing in a controlled, single-round setting in the Peano formal environment, across propositional logic, abelian groups, and natural-number multiplication, evaluating a set of conjectures by how much a fixed prover improves on held-out theorems after training on their proofs. We show that a far simpler generator does better: making small structural edits to statements the prover already knows yields conjectures that, at an equal training budget and under best-first search, improve the prover by 6 to 13 percentage points more than Minimo's learned conjectures. The gain holds even when conjectures are drawn at random from the generated pool. In contrast to the common practice of selecting the most difficult statements, we also propose Hard Neighbours (HN), a score that favors conjectures whose proof difficulty grows disproportionately relative to their structural distance from easier reference statements; HN gives the largest selection gains in propositional logic, but no selection method is best in every domain. In the current setting, how conjectures are generated matters more than how they are selected, and structural perturbation is the baseline that future conjecturers should be measured against. Apart from improvements in proving ability, we also study other attributes of generated proofs: the amount of search required and the length of the proofs.