PeopleofSuperintelligence

Researcher

Wojciech Nawrocki

Also known as Wojtek Nawrocki

Wojciech Nawrocki is a computer scientist who develops user interfaces for the Lean 4 theorem prover, and whose research covers interactive theorem proving, SAT solving and AI for math. After an MPhil thesis at the University of Cambridge in 2020, he moved to Carnegie Mellon, where he worked with Jeremy Avigad. He coauthored the paper on Lean's extensible interface and the ProofWidgets 4 library in 2023, a verified model-counting toolchain in Lean 4 in 2023, and a Lean verification of the empty hexagon number in 2024. He defended his PhD and joined the Lean FRO in March 2026, where he is a Senior Research Software Engineer.

Timeline

  1. 2020

    An MPhil at Cambridge

    He writes an MPhil thesis at the University of Cambridge in 2020, titled "Decidability of typechecking in a dependently-typed programming language with sigma types".

  2. 2021

    Local search for Brent equations

    In 2021, he coauthors "XOR Local Search for Boolean Brent Equations" with Zhenjun Liu, Andreas Fröhlich, Marijn Heule and Armin Biere, a paper at the SAT 2021 conference.

  3. 2023

    ProofWidgets and the Lean interface

    In 2023, he coauthors "An Extensible User Interface for Lean 4" with Edward Ayers and Gabriel Ebner. The interface comes with the ProofWidgets 4 library of UI components and is part of the core Lean distribution. He also completes an MS thesis at Carnegie Mellon in 2023, "User interfaces for computer-assisted mathematics".

  4. 2023–2025

    Verified model counting in Lean

    In 2023, he coauthors "Certified Knowledge Compilation with Application to Verified Model Counting" with Randal Bryant, Jeremy Avigad and Marijn Heule. Its checker and model counter are verified in Lean 4 and form the first formally verified toolchain for weighted and unweighted model counting, and an extended version appears in the Journal of Artificial Intelligence Research in 2025.

  5. 2024

    The empty hexagon in Lean

    In 2024, he coauthors a Lean verification of the empty hexagon number with Bernardo Subercaseaux, James Gallicchio, Cayden Codel, Mario Carneiro and Marijn Heule. It verifies that every set of 30 points in the plane in general position contains an empty convex hexagon, a result first settled with a SAT solver, and appears at ITP 2024.

  6. 2025–2026

    HoTTLean and SynthLean

    In 2025, he is among the authors of "HoTTLean: Formalizing the Meta-Theory of HoTT in Lean" with Joseph Hua, Steve Awodey, Mario Carneiro and others. In 2026, he is first author of the CPP 2026 paper "A Certifying Proof Assistant for Synthetic Mathematics in Lean", which presents SynthLean.

  7. 2026

    A Carnegie Mellon PhD

    He defends his PhD in Logic, Computation, and Methodology at Carnegie Mellon in March 2026, with Jeremy Avigad as supervisor, and the degree is dated May 2026. His thesis is "Three certificates in computer-assisted mathematics: Empty hexagons, model counting, and categorical semantics", and his focus is computer-aided reasoning, including interactive theorem proving, SAT solving and AI for math.

  8. Since March 2026

    Senior engineer at the Lean FRO

    He joins the Lean Focused Research Organization in March 2026 and develops user interfaces for the Lean 4 theorem prover there. He is a Senior Research Software Engineer on the Lean FRO team.

Career

  1. Since 2026Lean Focused Research OrganizationSenior Research Software Engineer

Education

  1. 2026Carnegie Mellon UniversityPhD in Logic, Computation, and Methodology
  2. 2023Carnegie Mellon UniversityMS
  3. 2020University of CambridgeMPhil

From the biography.

  1. Google has the highest combined h-index among AI organizationsIncludes Convergent Research. We estimate that Google holds the highest combined h-index at 8,016, while universities account for 73% of the deduplicated total across AI organizations.
  2. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionIncludes Carnegie Mellon University. We estimate where the people shaping AI studied and where their careers led. Massachusetts Institute of Technology leads with 467 former students, including 291 recorded doctorates.
  3. The company share of AI researchers’ top papers was 31% in 2020–2024 and 8% in 1970–1974Includes Carnegie Mellon University. We estimate where the people shaping AI worked when their most-cited papers appeared: the company share was 31% in 2020–2024 and 8% in 1970–1974, and Google led all organizations in 2020–2024.
  4. The median h-index is 48 at universities and 14 at frontier AI labsIncludes Carnegie Mellon University. The median h-index is 48 at universities and 14 at frontier AI labs. We compare publishing careers, recent citations, dual appointments and job moves across 2,420 university researchers and 308 frontier-lab researchers.

Colleagues

People named in this biography, and people with dated positions at the same organization in the same years.

Sources and credits

Photo: We have no published photo of Wojciech Nawrocki yet. Send us a free-licensed photo.

  1. Home | void main voidma.in. Checked 20 October 2026.
  2. An Extensible User Interface for Lean 4 drops.dagstuhl.de. Checked 20 October 2026.
  3. Certified Knowledge Compilation with Application to Verified Model Counting drops.dagstuhl.de. Checked 20 October 2026.
  4. [2403.17370] Formal Verification of the Empty Hexagon Number arxiv.org. Checked 20 October 2026.
  5. A Certifying Proof Assistant for Synthetic Mathematics in Lean (CPP 2026) - POPL 2026 popl26.sigplan.org. Checked 20 October 2026.
  6. Jeremy Avigad's Home Page andrew.cmu.edu. Checked 20 October 2026.
  7. Team — Lean Lang lean-lang.org. Checked 20 October 2026.