Target-Driven Automated Conjecturing for Neural Theorem Proving

Specialised neural theorem proving systems are commonly trained through reinforcement learning on large collections of formal problems, often autoformalised from human-written sources. This dependence on human-curated data limits their scalability and prevents theorem-proving agents from improving autonomously through mathematical exploration, since each new training curriculum must ultimately be supplied by humans. To address this challenge, we introduce TACO (Target-Driven Automated Conjecturing), a framework that constructs theorem-proving curricula from model-generated conjectures. Since individual conjectures have small and noisy training effects, TACO evaluates them collectively: starting from a small seed set, it generates candidate conjecture sets, trains Prover variants on them, and scores each set by the improvement its corresponding Prover achieves on a fixed target set. This evolutionary procedure builds the curriculum stage by stage while iteratively updating the seeds and base Prover. Across four mathematical domains, using held-out problems selected from publicly available Lean datasets, TACO increases the number of held-out test problems solved within 32 attempts from 10/128 to 43/128 after ten iterations, while successful proof attempts increase from 16/4096 to 358/4096. These results demonstrate that model-generated conjectures can provide effective training curricula, enabling theorem proving systems to improve through targeted mathematical exploration while reducing reliance on human-written problems.