Tutorial: Theorem Proving in Lean

Disclaimer: I am one of the maintainers of the web tutorial.

Thanks for posting this!

This tutorial is being used as a textbook for the 'Interactive Theorem Proving' course at Carnegie Mellon University (http://leanprover.github.io/cmu-15815-s15). It's mainly written by Prof. Jeremy Avigad (CMU) and Leonardo de Moura (MSR), with help of many contributors. While the course is listed as a graduate-level course, I think the tutorial is kindly written and readable for one who has basic understanding in logic and wants to learn more about interactive theorem proving. In fact, we do have undergraduate students in the class taking this course for credits as well.

The tutorial is (and will be) including the following topics:

   - dependent data types
   - type theory as a proof language
   - inductive data types
   - declarative vs. tactic-based proof style
   - classical vs. constructive logic
   - encodings of structures and type classes
   - elaboration and unification algorithms
   - homotopy type theory
   - ...

The course is based on a new open-source theorem prover, Lean (http://leanprover.github.io), developed at Microsoft Research.

We've tried hard to make the tutorial on 'Interactive Theorem Proving' really interactive. It contains many examples and exercises, and we provide an environment where you can load, modify, and execute code blocks. Technically, we use emscripten to compile C++ code into JavaScript. As a result, everything is running on a web-browser without a server-side help.

PDF version of the tutorial is also available: https://leanprover.github.io/tutorial/tutorial.pdf

The tutorial is still in-progress and your contributions are welcome. We host the repository at https://github.com/leanprover/tutorial . Please feel free to open an issue or make a pull request if you find typos or have suggestions.