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.
Email: unhex("776a6e6177726f636b6940636d752e656475")
PGP: 0925 028C 960A C24C FC57 8D9D 4E27 C2EB C32B 69B7
Publications
-
Formal Verification of the Empty Hexagon Number
Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule (2024)
In Interactive Theorem Proving - ITP 2024
[ pdf, code, doi ] -
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
[ pdf,
extended version,
code,
slides,
doi
]
-
An Extensible User Interface for Lean 4
Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner (2023)
In Interactive Theorem Proving - ITP 2023
[ pdf, code, doi ] -
An Impossible Asylum
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, and Wojciech Nawrocki (2023)
In The American Mathematical Monthly
[ pdf, doi ] -
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
[ pdf, code, slides, talk, doi ]
Theses
-
User interfaces for computer-assisted mathematics
Wojciech Nawrocki (2023)
MS thesis at Carnegie Mellon University
[ pdf ] -
Decidability of typechecking in a dependently-typed programming language with sigma types
Wojciech Nawrocki (2020)
MPhil thesis at the University of Cambridge
[ pdf, code ]
Books
-
Logic and Mechanized Reasoning
Jeremy Avigad, Marijn J.H. Heule, and Wojciech Nawrocki (2021)
[ page ]
News
- April 2025. Attending AI for Mathematics and Theoretical Computer Science at Simons and SLMath as a teaching assistant.
- June 2024. I presented ProofWidgets4 at Bonn HIM [ slides, video, video ].
- June 2024. I will be at the Prospects of Formal Mathematics trimester program in Bonn from June 17th until July 12th.
- May 2024. I presented ProofWidgets4 at the MIT PL Review [ video ].
- February 2023. I am honored to attend the IPAM workshop on Machine Assisted Proofs.
Posts
- [cr0wn] 0CTF/TCTF 2020 Finals: Oblivious (crypto) - September 26, 2020
- Supersingular isogeny key exchange for beginners - July 3, 2020
- TokyoWesterns CTF 5th 2019: Happy! (Crypto, 242 pts, 36 solves) - September 1, 2019
- Google CTF 2019 (Quals): Sandstone (Sandbox, 383 pts, 8 solves) - June 24, 2019
- HITCON CTF Quals 2018: Children Tcache (pwn, 246 pts) - October 20, 2018
- ECSC 18 Polish Junior Quals: keybd.py - June 22, 2018