Zulip Chat Archive

Stream: new members

Topic: Tutorials update


Patrick Massot (May 03 2020 at 21:12):

This is a message to all people from this stream who are still beginning to learn Lean. While waiting for more ambitious documentation projects, I translated all exercises from my first year undergrad course about proofs using Lean, and dumped them into the tutorials project. You can read instructions about how to use them in the README.

There are 81 exercises there, culminating with a proof of the intermediate value theorem (assuming existence of suprememums).
Don't hesitate to ask questions or open PRs, especially fixing my English. I translated really quickly and I wouldn't be surprised if there are whole sentences in French somewhere.

Patrick Massot (May 03 2020 at 21:12):

For people curious about teaching,: the main differences with the files I actually used with my students are:

  • I removed some explanations (partly because I was too lazy to translate, partly because I assume more math knowledge from you)
  • I added quite a bit on compressing tactics (I don't teach the anonymous constructor syntax, nor rintros or rcases in my course, trying to keep the syntactic load under control)

ROCKY KAMEN-RUBIO (May 04 2020 at 21:01):

Patrick Massot said:

This is a message to all people from this stream who are still beginning to learn Lean. While waiting for more ambitious documentation projects, I translated all exercises from my first year undergrad course about proofs using Lean, and dumped them into the tutorials project. You can read instructions about how to use them in the README.

There are 81 exercises there, culminating with a proof of the intermediate value theorem (assuming existence of suprememums).
Don't hesitate to ask questions or open PRs, especially fixing my English. I translated really quickly and I wouldn't be surprised if there are whole sentences in French somewhere.

Vous traduisez du français? Je pourrais peut-être vous aider.


Last updated: Dec 20 2023 at 11:08 UTC