# Learning Formal Mathematics From Intrinsic Motivation

arXiv: https://arxiv.org/abs/2407.00695 · HTML: https://mlsanity.com/paper/2407.00695/

## Key facts

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

## Builds on (most cited first, 30 of 30)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Zero-Shot Text-to-Image Generation](https://mlsanity.com/paper/2102.12092/) (2021)
- [Curiosity-driven Exploration by Self-supervised Prediction](https://mlsanity.com/paper/1705.05363/) (2017)
- [Hindsight Experience Replay](https://mlsanity.com/paper/1707.01495/) (2017)
- [Exploration by Random Network Distillation](https://mlsanity.com/paper/1810.12894/) (2018)
- [STaR: Bootstrapping Reasoning With Reasoning](https://mlsanity.com/paper/2203.14465/) (2022)
- [Large Language Models Can Self-Improve](https://mlsanity.com/paper/2210.11610/) (2022)
- [Unifying Count-Based Exploration and Intrinsic Motivation](https://mlsanity.com/paper/1606.01868/) (2016)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Synchromesh: Reliable code generation from pre-trained language models](https://mlsanity.com/paper/2201.11227/) (2022)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Learning with AMIGo: Adversarially Motivated Intrinsic Goals](https://mlsanity.com/paper/2006.12122/) (2020)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Language Models Can Teach Themselves to Program Better](https://mlsanity.com/paper/2207.14502/) (2022)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Learning to Prove Theorems by Learning to Generate Theorems](https://mlsanity.com/paper/2002.07019/) (2020)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Learning to Play with Intrinsically-Motivated Self-Aware Agents](https://mlsanity.com/paper/1802.07442/) (2018)
- [Holophrasm: a neural Automated Theorem Prover for higher-order logic](https://mlsanity.com/paper/1608.02644/) (2016)
- [First Neural Conjecturing Datasets and Experiments](https://mlsanity.com/paper/2005.14664/) (2020)
- [Machine learning and information theory concepts towards an AI Mathematician](https://mlsanity.com/paper/2403.04571/) (2024)
- [Peano: Learning Formal Mathematical Reasoning](https://mlsanity.com/paper/2211.15864/) (2022)
- [MathZero, The Classification Problem, and Set-Theoretic Type Theory](https://mlsanity.com/paper/2005.05512/) (2020)

## Built on by (most cited first, 30 of 45)

- [Absolute Zero: Reinforced Self-play Reasoning with Zero Data](https://mlsanity.com/paper/2505.03335/) (2025)
- [Learning to Reason without External Rewards](https://mlsanity.com/paper/2505.19590/) (2025)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [A Survey of Mathematical Reasoning in the Era of Multimodal Large Language Model: Benchmark, Method & Challenges](https://mlsanity.com/paper/2412.11936/) (2024)
- [Endless Terminals: Scaling RL Environments for Terminal Agents](https://mlsanity.com/paper/2601.16443/) (2026)
- [JarvisEvo: Towards a Self-Evolving Photo Editing Agent with Synergistic Editor-Evaluator Optimization](https://mlsanity.com/paper/2511.23002/) (2025)
- [Scalable Reinforcement Post-Training Beyond Static Human Prompts: Evolving Alignment via Asymmetric Self-Play](https://mlsanity.com/paper/2411.00062/) (2024)
- [Solving Inequality Proofs with Large Language Models](https://mlsanity.com/paper/2506.07927/) (2025)
- [Boundless Socratic Learning with Language Games](https://mlsanity.com/paper/2411.16905/) (2024)
- [DISCOVER: Automated Curricula for Sparse-Reward Reinforcement Learning](https://mlsanity.com/paper/2505.19850/) (2025)
- [Scaling Self-Play with Self-Guidance](https://mlsanity.com/paper/2604.20209/) (2026)
- [Shoot First, Ask Questions Later? Building Rational Agents that Explore and Act Like People](https://mlsanity.com/paper/2510.20886/) (2025)
- [dafny-annotator: AI-Assisted Verification of Dafny Programs](https://mlsanity.com/paper/2411.15143/) (2024)
- [Lean Finder: Semantic Search for Mathlib That Understands User Intents](https://mlsanity.com/paper/2510.15940/) (2025)
- [SPARQ: Synthetic Problem Generation for Reasoning via Quality-Diversity Algorithms](https://mlsanity.com/paper/2506.06499/) (2025)
- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)
- [Learning to Disprove: Formal Counterexample Generation with Large Language Models](https://mlsanity.com/paper/2603.19514/) (2026)
- [GASP: Guided Asymmetric Self-Play For Coding LLMs](https://mlsanity.com/paper/2603.15957/) (2026)
- [Artificial Intelligence and the Structure of Mathematics](https://mlsanity.com/paper/2604.06107/) (2026)
- [A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam](https://mlsanity.com/paper/2504.04945/) (2025)
- [A Deep Dive into Scaling RL for Code Generation with Synthetic Data and Curricula](https://mlsanity.com/paper/2603.24202/) (2026)
- [Spend Wisely: Maximizing Post-Training Gains in Iterative Synthetic Data Bootstrapping](https://mlsanity.com/paper/2501.18962/) (2025)
- [Discovering New Theorems via LLMs with In-Context Proof Learning in Lean](https://mlsanity.com/paper/2509.14274/) (2025)
- [Learning Interestingness in Automated Mathematical Theory Formation](https://mlsanity.com/paper/2511.14778/) (2025)
- [Improving Text-to-Image Generation with Intrinsic Self-Confidence Rewards](https://mlsanity.com/paper/2603.00918/) (2026)
- [Learning to Reason with Insight for Informal Theorem Proving](https://mlsanity.com/paper/2604.16278/) (2026)
- [Neural Garbage Collection: Learning to Forget while Learning to Reason](https://mlsanity.com/paper/2604.18002/) (2026)
- [LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation](https://mlsanity.com/paper/2505.12031/) (2025)
- [A Theoretical Framework for Self-Play Theorem Proving Algorithms](https://mlsanity.com/paper/2606.01861/) (2026)

## 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.