Solutions to "Theorem Proving n LEAN 4" exercises

Stream: lean4

[Jordi Majó]

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

[Ioannis Konstantoulas]

I am not aware of one, but I have solved almost all exercises up to chapter 5, and plan to solve all exercises in the book. What does the author, devs, and community think about creating a github repo with solutions (perhaps multiple solutions contributed by many authors)? Would it help or hurt education?

[Bulhwi Cha]

I solved all exercises. Do you want me to create a Git repository containing my solutions?

[Patrick Massot]

This is a question for @Jeremy Avigad.

[Nicolas Rolland]

solutions are mostly useful, to me at least, if one can learn from the style of the proofs

[Jeremy Avigad]

It's o.k. by me!

[Ioannis Konstantoulas]

Nicolas Rolland said:

solutions are mostly useful, to me at least, if one can learn from the style of the proofs

I agree completely, which is why I think the github repo could include multiple proofs, possibly through PRs, as long as they are sufficiently distinct and informative (at the discretion of the owner).

[Bulhwi Cha]

I'm a bit busy, but I'll make the repository eventually.