Peano: Learning Formal Mathematical Reasoning

TL;DR

This paper introduces Peano, a formal environment for mathematical reasoning, demonstrating that inducing reusable abstractions and curricula accelerates problem-solving in algebra, mirroring human learning processes.

Contribution

The paper presents Peano, a novel theorem-proving environment that formalizes algebra problems and shows how inducing abstractions improves learning efficiency.

Findings

Reinforcement learning struggles with complex problems without abstractions.

Inducing reusable tactics enables solving all formalized algebra problems.

Recovered problem order aligns with human-designed curricula, enhancing learning speed.

Abstract

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.