my solutions to the exercises in "theorem proving in lean 4"

Stream: lean4

[Bulhwi Cha]

Jordi Majó said:

I am very new here. Does anyone know if there is a solutions document to the exercises in "Theorem Proving in LEAN 4"?

Here are my solutions to the exercises in "Theorem Proving in Lean 4."

• SourceHut: https://git.sr.ht/~chabulhwi/tpil-solutions
• GitHub: https://github.com/chabulhwi/tpil-solutions

Currently, it contains solutions to the exercises from Chapters 2–5. I've also included additional quizzes and examinations in this repository, along with my solutions to the questions in each quiz.

I'm adding my solutions to this Git repository while recording videos of me reading #tpil in Korean and uploading to my YouTube channel. At this rate, I'll finish the work next year. I didn't expect it'd take so much time.

[Bulhwi Cha]

Do you think it's worth the effort to create English subtitles for my videos? A 15-minute video contains about 260 clauses, and I have 50 videos that are 50 minutes long on average.

I'm not sure whether there would be people who don't understand Korean but would watch these videos with English subtitles to learn Lean.

[(deleted)]

Just provide Korean subtitles. I think Korean is a beautiful language.

[(deleted)]

By providing Korean subtitles, those who can't listen to the audio can read the subtitles, and those who don't speak Korean can put the subtitles into a translation engine. This way you serve everyone.

If you don't provide Korean subtitles, however, your content isn't accessible to many Koreans without headphones or earbuds.

[Bulhwi Cha]

I've added ten additional questions to my quiz for Chapter 7 of "Theorem Proving in Lean 4": https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/docs/en/quiz/chapter07.md.