GlimpseOfLean

Tech stack & purpose

GlimpseOfLean is an introduction to theorem proving in Lean designed for learners who want to get up to speed in a few hours to a full day. The project provides two learning tracks: a shorter path that moves quickly through proof examples, and a longer path with explanations and exercises covering foundational proof techniques before progressing to specialized topics in mathematics including sequence limits, ring theory, probability theory, and logic. Built in Lean, the repository can be accessed through multiple methods including a browser-based lean4web server, GitHub Codespaces, Gitpod, or local installation, with accompanying reference materials like a tactics cheatsheet.

Community & reference links

• Lean FRO
• here
• Mathematics in Lean
• lean4web server
• 01Rewriting
• 02Iff
• 03Forall
• 04Exists
• explanations and exercises file
• ClassicalPropositionalLogic
• GaloisAdjunctions
• IntuitionisticPropositionalLogic
• Probability
• RingTheory
• SequenceLimits
• the introduction file

Languages

Contributors

• 
  Patrick Massot83 commits · 219 followers
• 
  Pietro Monticone10 commits · 1,160 followers
• Kyle Miller10 commits
• 
  Floris van Doorn8 commits · 145 followers
• 
  Johan Commelin3 commits · 101 followers
• 
  Anne Baanen2 commits · 49 followers
• 
  Jon Eugster2 commits · 36 followers
• 
  Lorenzo Luccioli2 commits · 21 followers
• 
  Kevin Buzzard1 commits · 946 followers
• 
  Rémy Degenne1 commits · 32 followers
• BapMel1 commits
• 
  AxelBoldt1 commits · 1 followers
• 
  Bhavik Mehta1 commits · 156 followers
• 
  Lucas Bazante1 commits · 11 followers
• 
  Filippo A. E. Nuccio1 commits · 21 followers
• 
  Alan Wang1 commits · 11 followers