HEXAGONbeta

Automated Conjecturing: Generation, Selection and Evaluation

Primarily human-written textHuman understanding: all partscs.AI — Artificial Intelligence

Contributed by Ayush Agrawal ↗, Vedant Shah, Navin Goyal, Ankit Anand, Aaron Courville

Version 1 / Oct 29, 2026 / CC BY 4.0

Abstract

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.

References

  1. Anthropic. Claude Opus 4.8 System Card. 2026link
  2. Luke Bailey; Kaiyue Wen; Kefan Dong; Tatsunori Hashimoto; Tengyu Ma. Scaling Self-Play with Self-Guidance. 2026arXiv
  3. Simon Colton. Automated Theory Formation in Pure Mathematics. Distinguished dissertations. 2002link
  4. De Moura, Leonardo; Bjørner, Nikolaj. Z3: An efficient SMT solver. International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337–340. 2008
  5. Kefan Dong; Tengyu Ma. STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving. 2025arXiv
  6. Fajtlowicz, Siemion. On conjectures of Graffiti. Discrete Math., vol. 72, no. 1-3, pp. 113–118. 1988DOI
  7. Johansson, Moa; Dixon, Lucas; Bundy, Alan. Conjecture synthesis for inductive theories. Journal of automated reasoning, vol. 47, no. 3, pp. 251–289. 2011
  8. Guillaume Lample; Marie-Anne Lachaux; Thibaut Lavril; Xavier Martinet; Amaury Hayat; Gabriel Ebner; Aurélien Rodriguez; Timothée Lacroix. HyperTree Proof Search for Neural Theorem Proving. 2022arXiv
  9. Lenat, Douglas B. Automated theory formation in mathematics. Proceedings of the 5th International Joint Conference on Artificial Intelligence - Volume 2, pp. 833–842. 1977
  10. Novikov, Alexander; Vũ, Ngân; Eisenberger, Marvin; Dupont, Emilien; Huang, Po-Sen; Wagner, Adam Zsolt; Shirobokov, Sergey; Kozlovskii, Borislav; Ruiz, Francisco JR; Mehrabian, Abbas; others. Alphaevolve: A coding agent for scientific and algorithmic discovery. arXiv preprint arXiv:2506.13131. 2025
Show all 19 referencesShow fewer references
  1. OpenAI. Finite Time Blowup for Navier–Stokes. OpenAI. 2026link
  2. OpenAI. GPT-5.6 System Card. 2026link
  3. Poesia, Gabriel; Goodman, Noah D. Peano: learning formal mathematical reasoning. Philosophical transactions. Series A, Mathematical, physical, and engineering sciences, vol. 381, no. 2251, pp. 20220044. 2023
  4. Poesia, Gabriel; Broman, David; Haber, Nick; Goodman, Noah D. Learning formal mathematics from intrinsic motivation. Advances in Neural Information Processing Systems, vol. 37, pp. 43032–43057. 2024
  5. Stanislas Polu; Ilya Sutskever. Generative Language Modeling for Automated Theorem Proving. 2020arXiv
  6. Trinh, Trieu H; Wu, Yuhuai; Le, Quoc V; He, He; Luong, Thang. Solving olympiad geometry without human demonstrations. Nature, vol. 625, no. 7995, pp. 476–482. 2024
  7. Vaswani, Ashish; Shazeer, Noam; Parmar, Niki; Uszkoreit, Jakob; Jones, Llion; Gomez, Aidan N; Kaiser, Łukasz; Polosukhin, Illia. Attention is all you need. Advances in neural information processing systems, vol. 30. 2017
  8. Wang, Mingzhe; Deng, Jia. Learning to prove theorems by learning to generate theorems. Advances in neural information processing systems, vol. 33, pp. 18146–18157. 2020
  9. Zeyu Zheng; Shengtong Zhang; Jeremy Avigad; Prasad Tetali; Sean Welleck. The Problem Is the Problem: Towards Scalable Mathematical Discovery. 2026arXiv

Version history

  1. v1Submitted by Ayush AgrawalInitial depositCurrentOct 28, 2026