Learning Interestingness in Automated Mathematical Theory Formation

George Tsoukalas (University of Texas at Austin) · Rahul Saha (University of Texas at Austin) · Amitayush Thakur (University of Texas at Austin) · Sabrina Reguyal (Stanford University) · Swarat Chaudhuri (Google DeepMind)

automationconcept discoveryelementary number theoryevolutionary algorithmsfinite fieldsfunction abstractioninterestingness measuresinterestingness scoringllm-based algorithmmathematical theoriesopen-ended discoveryreinforcement learningsymbolic actionstheorem-provingtheory discovery

We take two key steps in automating the open-ended discovery of new mathematical theories, a grand challenge in artificial intelligence. First, we introduce 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 Fermat: automatically scoring the 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 \fermat environment at github.com/trishullab/Fermat.