PatternMiner: Automated Mathematical Discovery Through LLM-Guided Training and Interpretation of Small Models

A large body of work in AI for math focuses on two approaches to mathematical discovery: the use of large language models (LLMs) to resolve well-specified conjectures and the use of small, narrow models for more open-ended, human-in-the-loop exploration. LLMs draw on broad mathematical knowledge to produce human-readable arguments, while small models support example-driven discovery by detecting patterns in computed examples. We present PatternMiner, a system in which an LLM agent generates exact datasets for a chosen problem, trains small models, and interprets what the models learn. The agent formulates conjectures, searches for counterexamples that prompt revisions, and uses hard-negative mining to select training examples that satisfy the current necessary conditions but fail the target property. The agent attempts proofs of conjectures that survive these tests. Applied to five problems in algebraic combinatorics, PatternMiner proves Schubert positivity and projection theorems, a character-row evaluation formula, restrictions on Kazhdan–Lusztig combinatorial invariance, and Schur positivity for a family of immanant coefficients; it also recovers classical Kronecker bounds.