This is the repository for my solutions to the exercises in "Theorem Proving in Lean 4" by Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, with contributions from the Lean Community. You are free to reuse the content under the terms of Apache License Version 2.0.
I've also included a quiz for each chapter of the text in this repository, along with my solutions to the questions in each quiz.
quizchapterXX.md: My additional quiz for Chapter XX of the text.
TPILChapterXX: Chapter XX of the text.Question*: Solutions to the question(s) of my quiz. Yet to be public.
If you've found errors in my solutions and want to fix them, please send an email to ~chabulhwi/[email protected]. It's my mailing list for end-user discussion and questions related to the lean-books project.