mlsanityData to 7 Oct 2026

Learning Formal Mathematics From Intrinsic Motivation

arXiv 2407.00695 ↗First posted 30 Jun 2024cs.AI cs.LOcited by 45

Not on the map. Why?

Abstract (arXiv)

How did humanity coax mathematics from the aether? We explore the Platonic view that mathematics can be discovered from its axioms - a game of conjecture and proof. We describe Minimo (Mathematics from Intrinsic Motivation): an agent that jointly learns to pose challenging problems for itself (conjecturing) and solve them (theorem proving). Given a mathematical domain axiomatized in dependent type theory, we first combine methods for constrained decoding and type-directed synthesis to sample valid conjectures from a language model. Our method guarantees well-formed conjectures by construction, even as we start with a randomly initialized model. We use the same model to represent a policy and value function for guiding proof search. Our agent targets generating hard but provable conjectures - a moving target, since its own theorem proving ability also improves as it trains. We propose novel methods for hindsight relabeling on proof search trees to significantly improve the agent's sample efficiency in both tasks. Experiments on 3 axiomatic domains (propositional logic, arithmetic and group theory) demonstrate that our agent can bootstrap from only the axioms, self-improving in generating true and challenging conjectures and in finding proofs.

Key facts. Cited by 45 papers in the map (data through 7 Oct 2026). Builds on 30 of its 48 references that are in the map. First posted on arXiv 30 Jun 2024.

Builds on

30 of 48 references.

References · 30

  1. 2017Attention Is All You Needcited by 59,932
  2. 2021Training Verifiers to Solve Math Word Problemscited by 9,743
  3. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  4. 2021Zero-Shot Text-to-Image Generationcited by 4,276
  5. 2017Curiosity-driven Exploration by Self-supervised Predictioncited by 1,173
  6. 2017Hindsight Experience Replaycited by 1,096
  7. 2018Exploration by Random Network Distillationcited by 966
  8. 2022STaR: Bootstrapping Reasoning With Reasoningcited by 895
  9. 2022Large Language Models Can Self-Improvecited by 656
  10. 2016Unifying Count-Based Exploration and Intrinsic Motivationcited by 632
  11. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  12. 2023Llemma: An Open Language Model For Mathematicscited by 385
18 more
  1. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  2. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  3. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  4. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  5. 2022Synchromesh: Reliable code generation from pre-trained language modelscited by 156
  6. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  7. 2020Learning with AMIGo: Adversarially Motivated Intrinsic Goalscited by 86
  8. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 80
  9. 2022Language Models Can Teach Themselves to Program Bettercited by 75
  10. 2018Reinforcement Learning of Theorem Provingcited by 69
  11. 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
  12. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  13. 2018Learning to Play with Intrinsically-Motivated Self-Aware Agentscited by 34
  14. 2016Holophrasm: a neural Automated Theorem Prover for higher-order logiccited by 29
  15. 2020First Neural Conjecturing Datasets and Experimentscited by 26
  16. 2024Machine learning and information theory concepts towards an AI Mathematiciancited by 20
  17. 2022Peano: Learning Formal Mathematical Reasoningcited by 15
  18. 2020MathZero, The Classification Problem, and Set-Theoretic Type Theorycited by 3

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 5; 2025: 19; 2026: 21.

45 papers.

Sort:

By area:

  1. 2025Absolute Zero: Reinforced Self-play Reasoning with Zero Datacited by 323
  2. 2025Learning to Reason without External Rewardscited by 199
  3. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  4. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  5. 2024A Survey of Mathematical Reasoning in the Era of Multimodal Large Language Model: Benchmark, Method & Challengescited by 55
  6. 2026Endless Terminals: Scaling RL Environments for Terminal Agentscited by 43
  7. 2025JarvisEvo: Towards a Self-Evolving Photo Editing Agent with Synergistic Editor-Evaluator Optimizationcited by 30
  8. 2024Scalable Reinforcement Post-Training Beyond Static Human Prompts: Evolving Alignment via Asymmetric Self-Playcited by 21
  9. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  10. 2024Boundless Socratic Learning with Language Gamescited by 12
  11. 2025DISCOVER: Automated Curricula for Sparse-Reward Reinforcement Learningcited by 11
  12. 2026Scaling Self-Play with Self-Guidancecited by 9
33 more
  1. 2024dafny-annotator: AI-Assisted Verification of Dafny Programscited by 8
  2. 2025SPARQ: Synthetic Problem Generation for Reasoning via Quality-Diversity Algorithmscited by 7
  3. 2025Lean Finder: Semantic Search for Mathlib That Understands User Intentscited by 7
  4. 2025Shoot First, Ask Questions Later? Building Rational Agents that Explore and Act Like Peoplecited by 7
  5. 2025Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoningcited by 6
  6. 2026GASP: Guided Asymmetric Self-Play For Coding LLMscited by 4
  7. 2026Learning to Disprove: Formal Counterexample Generation with Large Language Modelscited by 4
  8. 2025A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Examcited by 3
  9. 2026A Deep Dive into Scaling RL for Code Generation with Synthetic Data and Curriculacited by 3
  10. 2025Spend Wisely: Maximizing Post-Training Gains in Iterative Synthetic Data Bootstrappingcited by 2
  11. 2025Discovering New Theorems via LLMs with In-Context Proof Learning in Leancited by 2
  12. 2025Learning Interestingness in Automated Mathematical Theory Formationcited by 2
  13. 2026Artificial Intelligence and the Structure of Mathematicscited by 2
  14. 2026Learning to Reason with Insight for Informal Theorem Provingcited by 2
  15. 2026Neural Garbage Collection: Learning to Forget while Learning to Reasoncited by 2
  16. 2025LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generationcited by 1
  17. 2026Improving Text-to-Image Generation with Intrinsic Self-Confidence Rewardscited by 1
  18. 2026A Theoretical Framework for Self-Play Theorem Proving Algorithmscited by 1
  19. 2026Anchored Self-Play for Code Repaircited by 1
  20. 2026Formal Disco: Scalable Open-Ended Generation of Formally Verified Programscited by 1
  21. 2026Self-Play Pretraining with Zero Datacited by 1
  22. 2025Theoretical Barriers in Bellman-Based Reinforcement Learningcited by 0
  23. 2025Understanding Human Limits in Pattern Recognition: A Computational Model of Sequential Reasoning in Rock, Paper, Scissorscited by 0
  24. 2025HERAKLES: Hierarchical Skill Compilation for Open-ended LLM Agentscited by 0
  25. 2025Adaptable Hindsight Experience Replay for Search-Based Learningcited by 0
  26. 2026The Token Games: Evaluating Language Model Reasoning with Puzzle Duelscited by 0
  27. 2026Self-Supervised Theorem Discovery in a Formal Axiomatic Systemcited by 0
  28. 2026DecompRL: Solving Harder Problems by Learning Modular Code Generationcited by 0
  29. 2026ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Provingcited by 0
  30. 2026Direct Optimization of Generators for Search in Automated Theorem Provingcited by 0
  31. 2026Learning to Discover Interesting Mathematicscited by 0
  32. 2026CompassPlay: Rewarding the Proposer for Where It Moves the Solvercited by 0
  33. 2026LANTERN: Illuminating Hidden Mathematical Knowledge in Language Modelscited by 0