# Learning Interestingness in Automated Mathematical Theory Formation

arXiv: https://arxiv.org/abs/2511.14778 · HTML: https://mlsanity.com/paper/2511.14778/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 52 references that are in the map.
- First posted on arXiv 5 Nov 2025.

## Builds on (most cited first, 17 of 17)

- [Curiosity-driven Exploration by Self-supervised Prediction](https://mlsanity.com/paper/1705.05363/) (2017)
- [Unifying Count-Based Exploration and Intrinsic Motivation](https://mlsanity.com/paper/1606.01868/) (2016)
- [Eureka: Human-Level Reward Design via Coding Large Language Models](https://mlsanity.com/paper/2310.12931/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DreamCoder: Growing generalizable, interpretable knowledge with wake-sleep Bayesian program learning](https://mlsanity.com/paper/2006.08381/) (2020)
- [Symbolic Regression with a Learned Concept Library](https://mlsanity.com/paper/2409.09359/) (2024)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Top-Down Synthesis for Library Learning](https://mlsanity.com/paper/2211.16605/) (2022)
- [LILO: Learning Interpretable Libraries by Compressing and Documenting Code](https://mlsanity.com/paper/2310.19791/) (2023)
- [Learning Formal Mathematics From Intrinsic Motivation](https://mlsanity.com/paper/2407.00695/) (2024)
- [Meta-learning curiosity algorithms](https://mlsanity.com/paper/2003.05325/) (2020)
- [Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer](https://mlsanity.com/paper/1605.00723/) (2016)
- [The Ramanujan Machine: Automatically Generated Conjectures on Fundamental Constants](https://mlsanity.com/paper/1907.00205/) (2019)
- [First-Explore, then Exploit: Meta-Learning to Solve Hard Exploration-Exploitation Trade-Offs](https://mlsanity.com/paper/2307.02276/) (2023)
- [Automated conjecturing with TxGraffiti](https://mlsanity.com/paper/2409.19379/) (2024)

## Built on by (most cited first, 2 of 2)

- [Artificial Intelligence and the Structure of Mathematics](https://mlsanity.com/paper/2604.06107/) (2026)
- [Learning to Discover Interesting Mathematics](https://mlsanity.com/paper/2609.28603/) (2026)

## Abstract (arXiv)

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 this URL(https://github.com/trishullab/Fermat).