Introduction to using the Lean proof assistant

Igor Khavkine, Institute of Mathematics CAS

  https://users.math.cas.cz/~khavkine/lean-intro/talk-intro.html

Benefits of computer verified proofs

• Correctness
• Teaching proofs to computers (Machine Learning / Artificial Intelligence)
• Explaining proofs to humans
  • proofs are code and Large Language Models can explain code
    cf. my interactive experiment with the Nielsen-Schreier theorem
  • (experimental) software can translate Lean proofs to natural language, at any depth of detail

Lean proof assistant

Quanta Magazine 2021	Quanta Magazine 2023

Formal foundations: Type Theory

Set Theoretic

• set language: {}, { elems, ... }, elem set, ,
• logic language: , ; , , , ; ,
• rules of inference: ...

Type Theoretic

• Type language: term : type, func : type type (typed -calculus),
  write application as func arg₁ ... arg_n
• sets: sets are types (e.g., ), elems are terms,
  , , are funcs
• logic: props are types (e.g., , ), proofs are terms,
  , , , are funcs
• rules of inference: function composition

Inductive and dependent types

Induction / Recursion

• Creating types ex nihilo: define constants (cst_i : T), primitive functions (f_i : T ... T),
  freely apply primitive functions to constants and themselves
• Inductive Types: all terms are exhausted by formal function composition trees (well-founded recursion conditions must be satisfied); e.g., 0 : , succ : .

Dependent types

• Types are first class objects: type : Type, B-indexed families F : B Type are Dependent types
• Sum type / dependent disj.union: T = _{b : B} (F b) — like the total space of a fibration over B
• Product type / dependent product: T = _{b : B} (F b) — like the space of sections : B (_{b : B} F b)
• quantifiers: b : B, (P b) := _{b : B} P b,   b : B, (P b) := _{b : B} P b

Universes

• Russel's Girard's paradox: Type : Type implies a contradiction
• Solution: (Type ) : (Type ), index types by universe ; in Lean Prop : Type (‘-1’)

Lean: first steps

• Lean 4:
  • typed functional programming language
  • with strong dependent inductive types
  • unicode input (\to => , \pi => , ...), flexible self-defined syntax
  • proof irrelevance, classical logical axioms if needed (Choice, LEM)
• Installation: git, VS Code/Codium Lean 4 extension
• Live online: https://live.lean-lang.org/

Practical demo

• new project (VS Code -> -> New Project -> Using Mathlib)
• prove a simple proposition (theorem, proof state, goal)
  https://users.math.cas.cz/~khavkine/lean-intro/and-comm.lean
• prove a more complex theorem (Mathlib, tactics)
  https://users.math.cas.cz/~khavkine/lean-intro/cauchy-schwarz.lean

Learning Resources

• Natural Number Game
• Terry Tao's blog posts and phrasebook    
• Theorem Proving in Lean
• Mathematics in Lean
• Functional Programming in Lean

Search and Discovery

• Mathlib documentation
• Moogle free form search
• Loogle typed expression search
• Lean community Zulip chat