What Should a Theorem Prover See? Names, Notation, and Structure in Lean

Research on machine theorem proving has mostly improved models and search, and has paid less attention to a more basic choice: how a proof state is represented to the learner. The same proof state can be written in quite different surface forms, which may change the statistical structure a model can exploit. We study this problem in Lean, where a proof state can be written in several equivalent ways and every generated proof can be checked mechanically. We define a representation by three independent choices: identifiers (I), preserving or standardizing local variable and hypothesis names; core syntax (C), writing terms in conventional notation or in Lean’s elaborated core syntax; and relations (R), supplying or withholding explicit links between related parts of the state. We introduce ICR, a framework for controlled factorial experiments over these three factors. Training small encoder-decoder models from scratch on Mathlib proof states, with architecture, optimization, and examples held fixed, we compare all eight combinations of I, C, and R. We find that the representation has a large effect on theorem proving, and that the three factors behave very differently. For C, contrary to the common intuition that a more explicit input helps the learner, conventional mathematical notation consistently outperforms Lean’s elaborated core syntax: it improves prediction of the next step and proves 24 to 43% more unseen Mathlib theorems, a larger gain than nearly tripling the model size. This advantage persists even when both representations fit within the model context, so input length alone cannot explain it. For I, we find that models use statistical signal in identifier names: renaming variables and hypotheses more than halves, on average, the probability assigned to the author’s next proof step, even when that step does not mention them. Standardizing names removes this sensitivity, although its effect on proving theorems varies across benchmarks. For R, removing the explicit links from trained models barely changes the probability of the correct step, suggesting that providing structure does not mean that a model will use it. In our setting, the choice of representation mattered as much as a substantial increase in model scale, and sometimes more.