Hello! I’m Ben Przybocki, a first-year PhD student in computer science at CMU. My primary research interests are in automated reasoning and formal methods. I’m especially interested in using SAT and SMT solvers for computer-assisted mathematical discovery. I am supported by an NSF Graduate Research Fellowship.

I previously completed an MPhil in Advanced Computer Science at Cambridge, which was funded by a Churchill Scholarship. My master’s thesis, advised by Tobias Grosser, was on decision procedures for arithmetic problems, including implementations in the Lean proof assistant. Before that, I received a BS in mathematics from Stanford. My bachelor’s thesis, advised by Clark Barrett, studied theoretical aspects of SMT solving, namely theory combination and word equations. Earlier in my undergrad, I researched combinatorics.

If you want to talk about research, feel free to get in touch!