Introduction to proofs with Lean

This is an English translation of the exercises from the course “Logique et démonstrations assistées par ordinateur” at Paris-Saclay university. Those exercises have been designed in collaboration with Frédéric Bourgeois, Christine Paulin-Mohring and Valérie de Clippel.

It uses Lean and its controlled natural language library Verbose Lean.

A lot of text has been machine-translated, so don’t hesitate to point out weird things.

Also don’t hesitate to reach out if you want to use this for teaching. In particular, I can give you access to all the solution files.