Lean: First Steps

  • Home
  • Contents
  • Resources

Contents

Introduction

  • 00 - Proofs & Proof Assistants


Direct Proofs

  • 01 - First Proof
  • 02 - Substitution
  • 03 - Symbols, No Numbers
  • 04 - Simple Algebra
  • 05 - Inequalities

Structured Proofs

  • 06 - Intermediate Results
  • 07 - Proof By Cases
  • 08 - "And" Hypothesis
  • 09 - "Or" Goal
  • 10 - "And" Goal
  • 11 - Existence


Definitions & Lemmas

  • 12 - Odd & Even
  • 13 - Disequality
  • 14 - Disequality Again
  • 15 - Zero Product
  • 16 - Writing Our Own Lemma
  • 17 - Using Our Own Lemma
  • 18 - Our Own Definition

Interesting Proofs

  • 19 - Reductio Ad Absurdum
  • 20 - Contradictory Cases
  • 21 - Simple Induction
  • 22 - Recursion


Appendices

  • Appendix A - Taxonomy
  • Appendix B - Libraries


Email ThisBlogThis!Share to XShare to FacebookShare to Pinterest
Home
Subscribe to: Posts (Atom)

Links

  • Code on GitHub
  • YouTube Tutorials
  • Slides
  • Mechanics of Proof (Lean Tutorial)
  • Lean on the Web
  • Updating Lean+Mathlib

Search This Blog

Blog Archive

  • February 2025 (1)
  • January 2025 (1)
  • December 2024 (3)
  • November 2024 (5)
  • October 2024 (4)
  • September 2024 (5)
  • August 2024 (1)
  • July 2024 (2)
  • June 2024 (4)
  • May 2024 (1)
Powered by Blogger.