Post by Lisa Samoylov

My senior thesis won 2nd place in the Neukom Prize! The thesis explores an alternate way to represent Lean4 proofs, representing each proof based on how tactics affect the proof state, and whether that signal can guide existing theorem provers. Thanks to Prof. Soroush Vosoughi for his mentorship, and everyone who read drafts and offered suggestions. It wouldn't have been possible without you! 🤍 Part of this work was also accepted to ACL 2026 Student Research Workshop. See you in San Diego! ☀️