The Shape of Mathematical Creativity: Measuring Mathematical Exploration in Formal Proof Generation

Proof-generating systems return many candidates for the same theorem. Lean's kernel determines whether each candidate is correct, but not whether the candidates contain different mathematical reasoning. We study one measurable component of mathematical creativity: whether repeated successful generations explore distinct proof ideas rather than new formal expressions of the same idea. We analyze LeanRoute-216, which began with 36 kernel-verified and human-reviewed Lean proofs for 36 fixed propositions. Five additional proofs were then generated for each proposition with the goal of obtaining diverse proofs, producing 216 kernel-verified proofs in total. A graph-derived route-level review identified 61 diverse routes among the 216 distinct proof strings. This observation motivated a closer study of the distinction between formal variation and mathematical route diversity. Across the benchmark's 180 parent-candidate pairs, 25 were labeled as route changes and 155 as same-route comparisons. All pairs of candidate proofs were human-evaluated in a blinded second pass, with 95.6\% agreement with the original route-change labels ($\kappa=0.793$). Five theorem panels were used to refine the rubric and judging prompts, while the remaining 31 panels were held out for evaluation. On these 31 panels, LLM judges recognize route changes more reliably than lexical baselines, but remain substantially weaker at identifying the kind of change. These results support route diversity as an evaluation target separate from correctness and show how route-level auditing can inform proof search and the curation of synthetic reasoning data.