MathLoopBench (NeurIPS 2026 Workshop)

Our paper, MathLoopBench: Evaluating Agentic Mathematical Discovery Loops, has been accepted to the 6th Workshop on Mathematical Reasoning and AI (NeurIPS Workshop MATH-AI) 2026! [Paper]

This paper presents a benchmark for mathematical discovery loops, which must decide what is worth proving before proving it. Each loop grows a small Lean 4 library under a fixed budget and is scored by how many hidden target theorems it recovers.