tpil-solutions

English | 한국어[Korean]

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.

I use OmegaT to translate English documentation into Korean. The OmegaT project is in the docs directory. You need to install the Okapi filters plugin for OmegaT to make OmegaT parse Markdown files.

Directories and files

• docs: Markdown documents including notes and quizzes.

  • en: Source documents written in English.
    • notes
      • ChapterXX: My notes about the concepts explained in Chapter XX of the text.
    • quiz
      • chapterXX.md: My additional quiz for Chapter XX of the text.
  • ko: Korean translation of the source documents in the en directory. It has the same subdirectory structure as en.

• TPIL: My solutions to the exercises and questions.

  • ChapterXX: Chapter XX of the text.
    • Question*: Solutions to the question(s) of my quiz.

Contributing

If you've found errors in my solutions and want to fix them, please send an email to ~chabulhwi/lean-books-discuss@lists.sr.ht. It's my mailing list for end-user discussion and questions related to the lean-books project.