Learning Interestingness in Automated Mathematical Theory Formation
This work addresses the grand challenge of open-ended mathematical discovery for AI researchers, representing an incremental step with a new environment and algorithm.
The paper tackles the problem of automating mathematical theory discovery by introducing FERMAT, a reinforcement learning environment for concept discovery and theorem-proving, and develops an LLM-based evolutionary algorithm to score the interestingness of mathematical objects, achieving notable improvements over baselines in elementary number theory and finite fields.
We take two key steps in automating the open-ended discovery of new mathematical theories, a grand challenge in artificial intelligence. First, we introduce $\emph{FERMAT}$, a reinforcement learning (RL) environment that models concept discovery and theorem-proving using a set of symbolic actions, opening up a range of RL problems relevant to theory discovery. Second, we explore a specific problem through $\emph{FERMAT}$: automatically scoring the $\emph{interestingness}$ of mathematical objects. We investigate evolutionary algorithms for synthesizing nontrivial interestingness measures. In particular, we introduce an LLM-based evolutionary algorithm that features function abstraction, leading to notable improvements in discovering elementary number theory and finite fields over hard-coded baselines. We open-source the $\emph{FERMAT}$ environment at this URL(https://github.com/trishullab/Fermat).