Modeling Tactics as Operators: Effect-Grounded Representations for Lean Theorem Proving (2025)

Abstract: Interactive theorem provers (ITPs) such as Lean expose proof construction as a sequence of tactics applied to proof states. Existing machine learning approaches typically treat tactics either as surface tokens or as labels conditioned on the current state, eliding their operator-like semantics. This paper introduces a representation learning framework in which tactics are characterized by the changes they induce on proof states. Using a stepwise Lean proof corpus, we construct delta contexts —token-level additions/removals and typed structural edits—and train simple distributional models ( \Delta -SGNS and CBOW- \Delta ) to learn tactic embeddings grounded in these state transitions. Experiments on tactic retrieval and operator-style analogy tests show that \Delta -supervision yields more interpretable and generalizable embeddings than surface-only baselines. Our findings suggest that capturing the semantics of tactics requires modeling their state-transformational effects, rather than relying on distributional co-occurrence alone.

## introduction & related work interactive theorem provers (itps) such as lean expose proof construction as a sequence of tactics that transform a proof state, the local context and current goal(s), until all goals are discharged. learning to select or synthesize tactics has therefore become a central problem in neural theorem proving, with notable progress in hol4, hol light, and coq through systems such as tactictoe, holist, and coqgym @xcite @xcite . in parallel, leandojo has catalyzed research around lean by providing an open, reproducible environment, datasets, and retrieval-augmented provers @xcite . yet, most existing approaches model tactics either as labels to be predicted from the current state or as tokens in tactic sequences, rather than as operators that cause state change. this elides the essential semantics of tactics, "what they do to the proof state?," and can yield brittle representations tied to surface forms, local names, or co-occurrence statistics. ## experiments and results our goal is to verify the central hypothesis that a tactic is defined by its effect on the proof state. to attribute performance to specific sources of signal and to rule out alternative explanations (e.g., sequence co-occurrence or name leakage), we run three ablations that toggle which ∆-features are visible to the model: (1) tokens-only -contexts contain only added surface tokens (tok_w). this tests whether surface additions alone suffice to identify tactics. ## discussion and conclusion this paper introduced a representation-learning perspective in which tactics are modeled as operators defined by their effects on proof states. by leveraging ∆-supervision-token-level additions/removals and typed structural edits-we trained lightweight cbow and skip-gram models that learn embeddings grounded in state transitions. our experiments demonstrated that these embeddings capture tactic semantics more robustly than surface-only or sequence-based baselines. typed edits, in particular, provided complementary information that improved generalization and interpretability, enabling operator-style behaviors such as tactic-family clustering and state-translation analogies. beyond empirical gains, the central contribution lies in showing that surface-level distributional regularities, often sufficient in natural language modeling, are inadequate for theorem proving. capturing the semantics of tactics requires effect-grounded representations that model the transformations they induce. while our models are deliberately minimal, they establish a lightweight, interpretable bridge between symbolic proof states and neural methods, complementary to large-scale llm fine-tuning and retrieval-augmented provers. these findings motivate future work on scaling ∆-supervision to larger datasets, enriching structural edits, and integrating operator embeddings into end-to-end proof search systems.