ML for formal reasoning
I am a UW third-year undergraduate studying CS and Math and doing research into neural network verification.
ICLR 2026
Talk to me about my research, neural theorem proving, or today's invited talk.
The VerifAI-2 workshop runs April 26 in Room 208. If you are also there, please pay me a visit.
About
I am early in my research career, and looking to explore new directions. I have some experience with the Lean theorem prover, and I’m currently working on projects related to neural network verification.
At UW, I am especially interested in learning more about the theory behind neural networks, programing languages, and verification.
Publications
arXiv, 2026
Evan Wang, Simon Chess, Sophie Szeto, and Theodore Meek.
We study failure-triggered learned interventions inside Lean 4's grind tactic, including a cost-aware e-match filter and bounded lookahead for case splitting.
arXiv, 2026
Theodore Meek, Siyuan Ge, Di Qiu Xiang, Simon Chess, and Vasily Ilin.
We formalize numerical analysis with a coding-agent pipeline and introduce a reproducible quality audit that goes beyond Lean kernel acceptance.
ICLR VerifAI Workshop, 2026
Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge, Ajit Mallavarapu, Jarod Alper, and Vasily Ilin.
The paper introduces APRIL, a dataset for learning Lean proof repair from erroneous proofs, compiler diagnostics, repaired proofs, and feedback-grounded explanations.
Connect