Tutorials update

Stream: new members

[Patrick Massot]

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]

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]

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.