Resources about the Lean Theorem Prover (version 3)

• Lean Community — homepage of the lean community
• Lean Community Chat
• Documentation for mathlib
• Lean 3 for Hackers How to write programs in lean, like you would in Haskell. Note that the support for this in Lean 4 is much better.
• Lean3 Tactics

Learning Lean For Fun

• * Lean Tutorial For Mere Mortals (blog post) (code)
• Natural Number Game
• Real Number Game
• Complex Number Game

Courses using Lean

• Introduction to proofs with Lean

Books

• Mathematics in Lean — Mostly for mathematicians.
• Theorem Proving in Lean — The de facto reference book, not really for mathematicians nor for computer scientists.
• Logic and Proof also for mathematicians or people new to logic and theorem proving
• Hitchhiker’s guide to Logic Verification — for Computer Scientists

Other Resources

• Lean Tactic Cheat Sheet
• Miscellaneous Lean Code

• Lean Type Theory

• Lean-GPTF use neural networks to autocomplete your proofs. Requires OPEN_AI key, which I have :-)

Exams and Exercise Sheets in Lean

• Logical Verification in Lean

• Introduction to Proofs

• Foundations of Analysis
• Analysis I
• Algebraic Geometry
• Mathematical Structures

PhD and Master Thesis using Lean

• Verification of GPU Program Optimizations in Lean by Björn Fischer
• Formally Verified Insertion of Reference Counting Instructions by Marc Huisinga
• Strong Normalization of the Lambda Calculus in Lean by Sarah Mameche

More links

• Full list of Lean references

Short tips

code. set_option pp.generalized_field_notation false

Turns off dot-notation