Hi! My name is Wojtek (/ˈvɔj.tɛk/, like in envoy and techno). I develop user interfaces for the Lean 4 theorem prover at the Lean FRO. This is my personal website.

I recently obtained a PhD from the Department of Philosophy at Carnegie Mellon University, supervised by Jeremy Avigad. I focused on computer-aided reasoning (interactive theorem proving, SAT solving, AI for math), type theory, and categorical logic. 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("776a6e406c65616e2d66726f2e6f7267")
PGP: BF97 141D A5B2 0C93 77AE A94A 3286 9E10 76FA B89A

Publications

  • A Certifying Proof Assistant for Synthetic Mathematics in Lean
    Wojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, Steve Awodey (2026)
    In Certified Programs and Proofs - CPP 2026
    [ pdf, code, slides, talk, doi ]
  • 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, slides, 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, code, slides, doi ]
    Extended in the Journal of Artificial Intelligence Research - JAIR 2025
    [ pdf, 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

  • Three certificates in computer-assisted mathematics: empty hexagons, model counting, and categorical semantics
    Wojciech Nawrocki (2026)
    PhD thesis at Carnegie Mellon University
    [ pdf, proposal ]
  • 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