Hi! My name is Wojtek (voy-tech, like in envoy and techno). Currently, I am a PhD student in the Department of Philosophy at Carnegie Mellon University supervised by Jeremy Avigad. My research is in interactive and automated theorem proving, programming languages, type theory, and mathematical logic. I am also a developer of the Lean 4 theorem prover. I have a long-time hobbyist interest in cryptography. This is my personal website. Check out my publications, posts, and writeups of CTF (a kind of cybersecurity competition) challenges.
Certified Knowledge Compilation with Application to Verified Model Counting
Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule (2023)
In Theory and Practice of Satisfiability Testing - SAT 2023
An Extensible User Interface for Lean 4
Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner (2023)
In Interactive Theorem Proving - ITP 2023
An Impossible Asylum
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, and Wojciech Nawrocki (2023)
In The American Mathematical Monthly
XOR Local Search for Boolean Brent Equations
Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn J.H. Heule, and Armin Biere (2021)
In Theory and Practice of Satisfiability Testing - SAT 2021, 417-435
Decidability of typechecking in a dependently-typed programming language with sigma types
Wojciech Nawrocki (2020)
MPhil thesis at the University of Cambridge
Logic and Mechanized Reasoning.
Jeremy Avigad, Marijn J.H. Heule, and Wojciech Nawrocki (2021).
[ page ]