一作ACL 2026Workshop· Natural Language Processing
Representing Lean Proofs as Trajectories in Latent Space
Elisaveta Samoylov · Soroush Vosoughi
摘要
Lean proofs are built as sequences of tactic-induced state transitions, yet learned models often represent proof steps primarily through tactic strings or raw proof-state text. Building on Delta Tokens, which encode a proof step by the local edit it induces between successive proof states, we tra...