--- title: "Peano: Learning Formal Mathematical Reasoning (2022)" description: "Poesia and Goodman propose Peano, a dependently typed language whose environment always offers… 9 references, cited by 6 papers here." authors: ["Gabriel Poesia", "Noah D. Goodman"] year: 2022 venue: "arXiv:2211.15864" source: "https://arxiv.org/abs/2211.15864" doi: "10.1098/rsta.2022.0044" arxiv: "2211.15864" licence: "CC BY 4.0 (arXiv)" licence_url: "https://creativecommons.org/licenses/by/4.0/" summary_licence: "Elamur Cosmic License" canonical: "https://research.elamur.ai/free/en/papers/poesia-2022-peano-learning-formal-mathematical-reasoning/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/poesia-2022-peano-learning-formal-mathematical-reasoning/) [home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2022](https://md.research.elamur.ai/free/en/papers/2022/page/6/) / Peano: Learning Formal Mathematical Reasoning # Peano: Learning Formal Mathematical Reasoning **Authors:** [Gabriel Poesia](https://md.research.elamur.ai/free/en/authors/gabriel-poesia/) and [Noah D. Goodman](https://md.research.elamur.ai/free/en/authors/noah-d-goodman/) · **Year:** 2022 · **Venue:** arXiv:2211.15864 · **Publisher:** [Royal Society](https://md.research.elamur.ai/free/en/publishers/royal-society/) · **Licence:** [CC BY 4.0 (arXiv)](https://creativecommons.org/licenses/by/4.0/) **Links:** [Publisher's page](https://doi.org/10.1098/rsta.2022.0044) · [PDF](https://arxiv.org/pdf/2211.15864v1) · [DOI 10.1098/rsta.2022.0044](https://doi.org/10.1098/rsta.2022.0044) · [arXiv 2211.15864](https://arxiv.org/abs/2211.15864) · [OpenAlex](https://openalex.org/W4379347591) **Citations:** 13 citations (OpenAlex, 2026-10-14) · [6](https://md.research.elamur.ai/free/en/papers/poesia-2022-peano-learning-formal-mathematical-reasoning/cited-by/) in our library, of the 149,439 papers whose bibliographies we read ## Summary Mainstream proof assistants like Lean, Coq and Isabelle allow infinitely many valid steps at each point, which complicates treating proof finding as search. Poesia and Goodman propose Peano, a dependently typed language whose environment always offers a finite set of actions. With it, they formalize axioms and exercises from five introductory algebra sections of Khan Academy, producing well-defined search tasks. An existing reinforcement learning method masters only the first two sections, because later solutions become too long to find by exploration. The authors add tactic induction: anti-unification extracts recurring patterns from the agent's own solutions and turns them into new higher-level actions. With this, the agent eventually solves every problem. When problems are ordered by dependencies among the learned tactics, the resulting sequence significantly agrees with Khan Academy's expert curriculum, and a second agent trained in that order learns faster. The work offers a computational account of how abstractions and curricula jointly drive mathematical learning and its transmission across generations. ## Key points - **Peano** is a theorem-proving language built on dependent types (propositions as types, proofs as programs). Its search environment keeps the action space finite at every step. - **Benchmark:** 5 sections of the Khan Academy beginning-algebra curriculum, with axioms and exercises encoded in Peano. Agents start with no solving strategies beyond the axioms. - **Tactic learning:** the baseline RL agent stalls after the first two sections. Tactics induced via anti-unification are short straight-line programs that can call axioms or other tactics, and they let the agent eventually solve all problems. - **Curriculum recovery:** problems were seen in random order during training, yet the learned tactics imply an order that matches Khan Academy's significantly. "Second-generation" agents trained on this recovered order learn significantly faster. - **Limitations and resources:** Peano has no intermediate lemmas (lambda terms) and no backward reasoning, and its tactics cannot express loops or conditionals. Code, data and configs are available at https://github.com/gpoesia/peano. *Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.* ## Institutions - [Stanford University](https://md.research.elamur.ai/free/en/universities/stanford-university/) — University, Stanford, United States · 567 works · 335,189 citations 📚 Shelves (2): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works 🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works ## Cite Cite as: Gabriel Poesia and Noah D. Goodman. 2022. Peano: Learning Formal Mathematical Reasoning. arXiv:2211.15864. The paper itself, not this page. BibTeX from the library's record of the work. ```bibtex @misc{poesia2022peano, title = {{Peano: Learning Formal Mathematical Reasoning}}, author = {Gabriel Poesia and Noah D. Goodman}, year = {2022}, doi = {10.1098/rsta.2022.0044}, eprint = {2211.15864}, archivePrefix = {arXiv}, url = {https://doi.org/10.1098/rsta.2022.0044} } ``` - [← previous Offensive Language Detection in Under-resourced Algerian Dialectal Arabic Language](https://md.research.elamur.ai/free/en/papers/boucherit-2022-offensive-language-detection-under-resourced/) - [next → Potential Idiomatic Expression (PIE)-English: Corpus for Classes of Idioms](https://md.research.elamur.ai/free/en/papers/adewumi-2022-potential-idiomatic-expression-pie-english/) - [↑ back to papers of 2022](https://md.research.elamur.ai/free/en/papers/2022/page/6/) ## References 9 references, 4 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet. 1. Thomas Anthony, Zheng Tian, and David Barber. [Thinking fast and slow with deep learning and tree search](https://md.research.elamur.ai/free/en/papers/anthony-2017-thinking-fast-slow-deep-learning/). Advances in Neural Information Processing Systems, 30, 2017. 2. Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, volume 97… — [HOList: An Environment for Machine Learning of Higher-Order Theorem Proving](https://md.research.elamur.ai/free/en/papers/bansal-2019-holist-environment-machine-learning-higher/) 3. Yoshua Bengio, Jérôme Louradour, Ronan Collobert, and Jason Weston. [Curriculum learning](https://md.research.elamur.ai/free/en/papers/bengio-2009-curriculum-learning/). In Proceedings of the 26th annual international conference on machine learning, pages 41–48, 2009. 4. Kyunghyun Cho, Bart van Merriënboer, Dzmitry Bahdanau, and Yoshua Bengio. On the properties of neural machine translation: Encoder–decoder approaches. Syntax, Semantics and Structure in Statistical Translation, page 103, 2014. — [On the Properties of Neural Machine Translation: Encoder-Decoder Approaches](https://md.research.elamur.ai/free/en/papers/cho-2014-properties-neural-machine-translation-encoder/) 5. Simon Colton, Alan Bundy, and Toby Walsh. On the notion of interestingness in automated mathematical discovery. International Journal of Human-Computer Studies, 53(3):351–375, 2000. [find](https://scholar.google.com/scholar?q=Simon+Colton%2C+Alan+Bundy%2C+and+Toby+Walsh%2E+On+the+notion+of+interestingness+in+automated+mathematical+discovery%2E+International+Journal+of+Human%2DComputer+Studies%2C+53%283%29%3A351%E2%80%93375%2C+2000%2E) 6. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, 1962. [find](https://scholar.google.com/scholar?q=Martin+Davis%2C+George+Logemann%2C+and+Donald+Loveland%2E+A+machine+program+for+theorem%2Dproving%2E+Communications+of+the+ACM%2C+5%287%29%3A394%E2%80%93397%2C+1962%2E) 7. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM (JACM), 7(3):201–215, 1960. [find](https://scholar.google.com/scholar?q=Martin+Davis+and+Hilary+Putnam%2E+A+computing+procedure+for+quantification+theory%2E+Journal+of+the+ACM+%28JACM%29%2C+7%283%29%3A201%E2%80%93215%2C+1960%2E) 8. Kevin Ellis, Catherine Wong, Maxwell Nye, Mathias Sablé-Meyer, Lucas Morales, Luke Hewitt, Luc Cary, Armando Solar-Lezama, and Joshua B Tenenbaum. Dreamcoder: Bootstrapping inductive program synthesis with wake-sleep library learning. In Proceedings of the 42nd acm sigplan international conference o… [find](https://scholar.google.com/scholar?q=Kevin+Ellis%2C+Catherine+Wong%2C+Maxwell+Nye%2C+Mathias+Sabl%C3%A9%2DMeyer%2C+Lucas+Morales%2C+Luke+Hewitt%2C+Luc+Cary%2C+Armando+Solar%2DLezama%2C+and+Joshua+B+Tenenbaum%2E+Dreamcoder%3A+Bootstrapping+inductive+program+synthesis) 9. William Timothy Gowers. – . . . - . 0000000 .......... [find](https://scholar.google.com/scholar?q=William+Timothy+Gowers%2E+%E2%80%93+%2E+%2E+%2E+%2D+%2E+0000000+%2E%2E%2E%2E%2E%2E%2E%2E%2E%2E) *Updated 3 November 2026*