TPIL - Adding Solutions

Stream: general

[Matteo Gätzner]

Hello everyone,

I'm currently learning to use lean for theorem proving and think it would be useful for people like me that use Theorem Proving in Lean 4 like a textbook with exercises to have solutions available to get unstuck. I'd propose to add a solutions.lean file (or multiple ones, one of each chapter) to the theorem_proving_in_lean4 repository, since I'm suspecting this is where people working through the exercises would first search for solutions.

A second alternative to this could be to provide a disclaimer somewhere in the document that they could ask for solutions in this community chat. However, this could lead to someone having to answer the same question over and over again.

A third alternative is to put solutions in the document itself, e.g. "13. Exercise Solutions".

If we go for option 1 or 3, I could provide solutions for the first 4 chapters.

What do you think?

[Gareth Ma]

I agree with option 1.

[Timo Carlin-Burns]

@David Thrane Christiansen, I believe you're the only reviewer for TPIL PRs, so if we started creating PRs adding solutions, the final review burden would be on you. What do you think?

[Timo Carlin-Burns]

If you're too busy to review thoroughly enough to ensure the solutions are high quality/clearly explained, a fourth option would be that community members could compile solutions in external repositories, and the book could link to a GitHub issue or zulip thread where readers could find links to those repositories

[Bulhwi Cha]

I can review those solutions, but I'm thinking of creating a repository of my solutions to all exercises of #tpil. I just don't have time to do it right now.

[David Thrane Christiansen]

I'm not the author of the book, only a maintainer, and the time I have to do that is fairly limited at the moment. I'd generally leave this kind of question up to an author. I'll follow up with them.

[Mario Carneiro]

I believe @Jeremy Avigad has solutions somewhere but not publicly. There is clearly some value in having a book for which solutions are not publicly available for teaching purposes.

[Mario Carneiro]

@Bulhwi Cha So I would advise against putting your solutions online for the same reason

[Mario Carneiro]

A second alternative to this could be to provide a disclaimer somewhere in the document that they could ask for solutions in this community chat. However, this could lead to someone having to answer the same question over and over again.

This already happens, it's fine. At least if a person is doing it we can do some bare checking of the questioner to see if this is a "do my homework for me" situation

[Jeremy Avigad]

IIRC, there were solutions to some of the problems in the source files to TPIL3, but I don't think they survived the port to TPIL4. If someone wants to set up an independent repository with solutions, I'd be happy to have a link to it from the TPIL4 cover page that credits the author. Is that a good solution? For something more integrally connected to the text, I'd prefer to be involved in the process -- but I doubt I can even take a look at this before the summer.

[Bulhwi Cha]

Mario Carneiro said:

I believe Jeremy Avigad has solutions somewhere but not publicly. There is clearly some value in having a book for which solutions are not publicly available for teaching purposes.

Bulhwi Cha So I would advise against putting your solutions online for the same reason

In South Korea, there's no professor teaching students Lean, so solutions to #tpil would be helpful to potential Korean autodidacts who want to learn Lean.

[Matteo Gätzner]

Bulhwi Cha said:

Mario Carneiro said:

I believe Jeremy Avigad has solutions somewhere but not publicly. There is clearly some value in having a book for which solutions are not publicly available for teaching purposes.

Bulhwi Cha So I would advise against putting your solutions online for the same reason

In South Korea, there's no professor teaching students Lean, so solutions to #tpil would be helpful to potential Korean autodidacts who want to learn Lean.

For the benefit of people self-learning Lean, I’d also be in favor of publishing solutions.

[Kevin Buzzard]

Just to give a counterpoint -- I learnt lean from #tpil and I'm sure that the fact that there were no solutions was really helpful to me, because it made me work everything out myself. I asked on the lean chat (then on gitter) when I got stuck. But we all learn in different ways.

[Bulhwi Cha]

I also solved most exercises in #tpil by myself and looked for the solutions to the ones I got stuck on in this Zulip chat. But I don't think everyone can do this.

Moreover, it's hard for most Koreans to communicate in English. Of course, you can't read #tpil if your English reading skills aren't good enough. That's why I'll translate the textbook into Korean in the future and then become the only Korean using it to teach other Koreans Lean.

[Matteo Gätzner]

Kevin Buzzard said:

Just to give a counterpoint -- I learnt lean from #tpil and I'm sure that the fact that there were no solutions was really helpful to me, because it made me work everything out myself. I asked on the lean chat (then on gitter) when I got stuck. But we all learn in different ways.

Fair point :)

[Kevin Cheung]

Bulhwi Cha said:

I also solved most exercises in #tpil by myself and looked for the solutions to the ones I got stuck on in this Zulip chat. But I don't think everyone can do this.

Moreover, it's hard for most Koreans to communicate in English. Of course, you can't read #tpil if your English reading skills aren't good enough. That's why I'll translate the textbook into Korean in the future and then become the only Korean using it to teach other Koreans Lean.

Have you set up a repository for the Korean translation?

[Bulhwi Cha]

Not yet. I'm thinking of using Sphinx to make a Korean translation of #tpil, but I don't know how to do it right now.

[Bulhwi Cha]

See #lean4 > will verso support internationalization?

[Bulhwi Cha]

I've released my solutions to the exercises in Chapter 3 of the text: https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/TPIL/Chapter03/Exercise01-03.lean.

I haven't yet uploaded them to the GitHub mirror of my repository called tpil-solutions.

I also created problems for an exam that covers Chapters 2 to 4 of the text, focusing on proving universal and existential statements: https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/TPIL/Exam/Exam01.lean.

I won't provide solutions to the problems on my exams, but my mentees will.