Neukom Fall Scholar Publication

Neukom Scholar Elisaveta (Lisa) Samoylov '26 at Dartmouth, paper "Modeling Tactics as Operators: Effect-Grounded Representations for Lean Theorem Proving" (with co-author Soroush Vosoughi) has been accepted to the 3rd workshop on Mathematical Natural Language Processing (MathNLP 2025) at EMNLP in Suzhou, China! Additionally it was nominated for an oral presentation.
In this work Samoylov tackles how interactive theorem provers like Lean treat proof strategies (tactics) and propose a new representation learning framework where tactics are modelled by their effects on proof states rather than just as surface tokens. We build "delta contexts" from Lean proof corpora, train supervised/unsupervised embedding models (Δ-SGNS, CBOW-Δ), and show improved interpretability and generalisation compared to conventional baselines.

Learn more here: https://aclanthology.org/2025.mathnlp-main.12/