# Peano: Learning Formal Mathematical Reasoning

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

## Key facts

- Cited by 15 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 12 of its 40 references that are in the map.
- First posted on arXiv 29 Nov 2022.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

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

- [Playing Atari with Deep Reinforcement Learning](https://mlsanity.com/paper/1312.5602/) (2013)
- [On the Properties of Neural Machine Translation: Encoder-Decoder Approaches](https://mlsanity.com/paper/1409.1259/) (2014)
- [Thinking Fast and Slow with Deep Learning and Tree Search](https://mlsanity.com/paper/1705.08439/) (2017)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Holophrasm: a neural Automated Theorem Prover for higher-order logic](https://mlsanity.com/paper/1608.02644/) (2016)
- [Contrastive Reinforcement Learning of Symbolic Reasoning Domains](https://mlsanity.com/paper/2106.09146/) (2021)
- [Lemma Mining over HOL Light](https://mlsanity.com/paper/1310.2797/) (2013)

## Built on by (most cited first, 15 of 15)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Building Machines that Learn and Think with People](https://mlsanity.com/paper/2408.03943/) (2024)
- [Evaluating Language Models for Mathematics through Interactions](https://mlsanity.com/paper/2306.01694/) (2023)
- [Learning Formal Mathematics From Intrinsic Motivation](https://mlsanity.com/paper/2407.00695/) (2024)
- [Forward-Backward Reasoning in Large Language Models for Mathematical Verification](https://mlsanity.com/paper/2308.07758/) (2023)
- [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025)
- [Exploring the hierarchical structure of human plans via program generation](https://mlsanity.com/paper/2311.18644/) (2023)
- [AI for Mathematics: A Cognitive Science Perspective](https://mlsanity.com/paper/2310.13021/) (2023)
- [What makes math problems hard for reinforcement learning: a case study](https://mlsanity.com/paper/2408.15332/) (2024)
- [Certified Deductive Reasoning with Language Models](https://mlsanity.com/paper/2306.04031/) (2023)
- [Quantifying artificial intelligence through algorithmic generalization](https://mlsanity.com/paper/2411.05943/) (2024)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [MathDSL: A Domain-Specific Language for Concise Mathematical Solutions Via Program Synthesis](https://mlsanity.com/paper/2409.17490/) (2024)
- [How are Scientific Concepts Birthed? Typing Rules of Concept Formation in Theoretical Physics Reasoning](https://mlsanity.com/paper/2509.10740/) (2025)
- [Reinforcement Learning for Symbolic Equation Solving](https://mlsanity.com/paper/2608.30162/) (2026)

## Abstract (arXiv)

General mathematical reasoning is computationally undecidable, but humans routinely solve new problems. Moreover, discoveries developed over centuries are taught to subsequent generations quickly. What structure enables this, and how might that inform automated mathematical reasoning? We posit that central to both puzzles is the structure of procedural abstractions underlying mathematics. We explore this idea in a case study on 5 sections of beginning algebra on the Khan Academy platform. To define a computational foundation, we introduce Peano, a theorem-proving environment where the set of valid actions at any point is finite. We use Peano to formalize introductory algebra problems and axioms, obtaining well-defined search problems. We observe existing reinforcement learning methods for symbolic reasoning to be insufficient to solve harder problems. Adding the ability to induce reusable abstractions ("tactics") from its own solutions allows an agent to make steady progress, solving all problems. Furthermore, these abstractions induce an order to the problems, seen at random during training. The recovered order has significant agreement with the expert-designed Khan Academy curriculum, and second-generation agents trained on the recovered curriculum learn significantly faster. These results illustrate the synergistic role of abstractions and curricula in the cultural transmission of mathematics.