I'm a Turing Scholar at UT Austin studying computer science and mathematics. I'm currently Co-founder of Truss Legal. Before that I worked on automated theorem proving in the UToPiA Lab, where I worked on making LLM-based provers better at Lean 4 by using RL to learn when to retrieve custom tactics.
Truss Legal — Deposition prep for litigators at YC
We help litigators draft deposition outlines, rehearse against a live witness, and prepare their own witnesses against a live opposing counsel. Afterward, they get a report on how it went.
UToPiA Lab, UT Austin — Undergraduate Researcher
Worked with Prof. Isil Dillig, Maxine Xin, and Prof. Elias Stengel-Eskin: made a dynamic retrieval system that injects relevant custom proof tactics into LLM-based theorem provers at inference time.
Lean 4 Directed Reading Program — Member
Functional programming and formal verification in Lean 4. Proved the termination of quicksort by hand, which is what got me interested in formal reasoning.
University of Texas at Austin — CS (Turing) + Mathematics