[dernett]

I'm going to try formalizing this course in Lean--not sure how hard it is going to be. If anyone is interested in doing the same, please feel free to contribute!

https://github.com/dernett/Lean61200J

[vkuncak77]

This sounds very interesting and relevant to the goals of the CSLib initiative that apparently just got started. I don't have a better public link to it now except this LinkedIn post (perhaps there's a Zulip tag):

https://www.linkedin.com/posts/lean-fro_leanlang-cslib-forma...

[monkeyelite]

What will that accomplish?

[amw-zero]

You can write proofs along with the course, and since they are machine checked you can have confidence that they are correct.

If you don't know, writing a proof in isolation can be difficult, since you may be writing on that isn't actually sound.