Hello! I’m Ben Przybocki, an incoming 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!