Learning Formal Mathematics From Intrinsic Motivation
Gabriel Poesia, David Broman, Nick Haber, Noah D. Goodman

TL;DR
This paper introduces Minimo, an agent that learns to generate challenging conjectures and prove theorems within axiomatic mathematical domains using intrinsic motivation, combining language models with proof search to self-improve over time.
Contribution
It presents a novel framework that jointly learns conjecture generation and theorem proving, enabling self-improvement in mathematical reasoning from axioms alone.
Findings
Successfully generated challenging conjectures in multiple domains
Demonstrated self-improvement in proof and conjecture generation
Achieved significant sample efficiency through hindsight relabeling
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
Taxonomy
TopicsMathematics Education and Teaching Techniques · History and Theory of Mathematics · Computability, Logic, AI Algorithms
