{"id":"hexagon/2610.00631","pdf":"https://hexagonmath.org/pdf/2610.00631v1","url":"https://hexagonmath.org/abs/2610.00631v1","tags":["msc:68T05","msc:68T99","conjecturing","language models"],"score":0,"title":"Automated Conjecturing: Generation, Selection and Evaluation","domain":"cs.AI","source":"hexagon","authors":["Ayush Agrawal","Vedant Shah","Navin Goyal","Ankit Anand","Aaron Courville"],"reviews":0,"subject":"cs.AI","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-10-29","reactions":{},"withdrawn":false,"authorship":"human","formalized":false,"human_understanding":"all"}