Papers by Elisaveta Samoylov

Copied to clipboard

Challenge:	Lean proofs are built as sequences of tactic-induced state transitions, but learned models often represent proof steps through tactic strings or raw proof-state text.
Approach:	They train an encoder-only Transformer to learn contextualized representations of Lean proof steps from state changes.
Outcome:	The proposed model yields better held-out next-tactic retrieval than a surface-syntax control . the results provide a promising basis for future trajectory-aware theorem proving .