Working with Lean 4

• Lean 4:
  • functional programming language
  • interactive theorem prover for
    • mathematics
    • software and hardware verification
  • based on dependent type theory
    • extension of Russels type theory
    • basic idea: sets always contain objects of a common type
• Lean structure:
  • minimal kernel implementing core type theory
  • tactics language for proof automation
  • library with fundamental types, e. g.
    • Natural Numbers (starting at 0)
    • Integers
    • Strings
    • Booleans
    • Arrays
    • Sets
  • Mathlib
    • huge library of basic and more advanced mathematics
• Installation:
  • installation guide
  • install VS Code
  • install Lean 4 VS Code extension
  • complete Lean 4 setup
    • create a new project using Mathlib
    • name arbitrary, e.g. demo
  • creates subfolder demo with (amongst others):
    • demo.lean, Demo/, Demo/Basic.lean
• Documentation:
  • Natural Number Game
    • basic theory of ℕ
  • Mathematics in Lean
    • formalizing mathematics
  • Theorem Proving in Lean 4
    • foundations of dependent type theory
  • a lot more
• Using exercise files:
  • create new Mathlib project exercises
  • copy lean files ComplexNumbers.lean, Continuity.lean, MatrixRank.lean into exercises/Exercises
  • copy lean file Exercises.lean into exercises
  • open ComplexNumbers
    • click Restart File
    • → file is evaluated
    • → No goals
    • everything ok
  • move cursor on beginning of L18
    • goal is shown as ⊢ ...
  • move cursor at beginning of L23
    • new hypotheses h1 is shown
    • goal has changed