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.

Most of the content has been released under the terms of Apache License Version 2.0. However, this repository also contains a Lean file in the public domain.

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. This directory also contains Lean files providing examples of the concepts discussed in the text.

  • 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/[email protected]. It's my mailing list for end-user discussion and questions related to the lean-books project.