Hi! My name is Wojtek (/ˈvɔj.tɛk/, like in envoy and techno). I am a final year PhD student in the Department of Philosophy at Carnegie Mellon University supervised by Jeremy Avigad. This is my personal website.

My research is in computer-aided reasoning (interactive theorem proving, SAT solving, AI for math), as well as type theory and categorical logic. I am also a developer of the Lean 4 theorem prover. I have previously worked at Harmonic, Microsoft Research Redmond, and SRI International.

Check out my publications, posts, and writeups of CTF challenges below.

Email: unhex("776a6e6177726f636b6940636d752e656475")
PGP: 0925 028C 960A C24C FC57 8D9D 4E27 C2EB C32B 69B7

Publications

  • HoTTLean: Formalizing the Meta-Theory of HoTT in Lean
    Joseph Hua, Steve Awodey, Mario Carneiro, Sina Hazratpour, Wojciech Nawrocki, Spencer Woolfson, and Yiming Xu (2025)
    In Types for Proofs and Programs - TYPES 2025
    [ extended abstract, code, slides, talk ]
  • 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
    Extended in the Journal of Artificial Intelligence Research - JAIR 2025
    [ pdf, extended version, code, slides, doi, journal 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, ..or is it? ]
  • 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, 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

Posts