Books

• Mathematical Logic and Computation
  In copyediting. To be published by Cambridge University Press. Table of contents and preface: pdf.

• Theorem Proving in Lean
  with Leonardo de Moura and Soonho Kong. Online: html, text: pdf.
• Theorem Proving in Lean 4
  with Leonardo de Moura, Soonho Kong, and Sebastian Ullrich. Online: html.
• Logic and Proof
  with Floris van Doorn and Robert Lewis. Online: html, text: pdf.
• Mathematics in Lean
  with Kevin Buzzard, Robert Lewis, and Patrick Massot (in progress). Online: html, text: pdf.
• Logic and Mechanized Reasoning
  with Marijn Heule and Wojciech Nawrocki (in progress). Online: html, text: pdf.
• The Lean Reference Manual
  with Leonardo de Moura, Gabriel Ebner, and Sebastian Ullrich. Online: html, text: pdf.

• Proceedings of Interactive Theorem Proving (ITP) 2018
  with Assia Mahboubi. SpringerLink.
• Proceedings of Certified Programs and Proofs (CPP) 2016
  with Adam Chlipala. doi.