A glimpse at Type Theory and a
    glance at the Lean Proof Assistant

Igor Khavkine, Institute of Mathematics CAS

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

A brief history of formal proofs: Leibniz (1600s)

Leibniz imagined a formal calculus for logical reasoning.

"[...] if controversies [about a proof] were to arise, there would be no more need of disputation between two philosophers mathematicians than between two calculators. For it would suffice for them to take their pencils in their hands and to sit down at the abacus, and say to each other (and if they so wish also to a friend called to help): Calculemus. (Let us calculate.)" — Wikiquote

A brief history ...: Russel & Whithead (1910s)

A brief history ...: Lean (2013– )

Leibniz's dream is (in a sense) realized:

theorem one_plus_one_is_two : 1 + 1 = (2 : Nat) :=
  (succ_eq_add_one 1).symm.trans (congrArg Nat.succ one_eq_succ_zero)

Of course, Lean is but one of many formal proof assistants that have been slowly bringing Leibniz's dream closer to reality since the introduction of digital computers (e.g., Metamath, Mizar, Isabelle, Coq/Rocq, ...).

Benefits of computer verified proofs

  • Certified correctness
    • peace of mind
    • mission critical software
    • trust in collaborations
  • 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

Why the Lean proof assistant? Because...
Quanta Magazine 2021 Quanta Magazine 2023
(feat Peter Scholze, Fields Medal 2018) (feat Terry Tao, Fields Medal 2006)

+ Lean's Mathlib is on track to become the largest library of formalized mathematics.

My humble contribution

Theorem (Vitali): A sequence of functions has a limit
in norm iff has a limit (in measure or a.e.) and is both uniformly integrable and uniformly tight.

uniform integrability: no concentration of measure locally
uniform tightness: no escape of measure to infinity (is automatic when )

Lean's Mathlib already had the version for . I extended it to cover the case .

Pull Request #9163: about 500 lines of Lean code

  • 20 Dec 2023: submitted
  • 21 Jul 2024: accepted after review

How does Lean work? Type Theory

  • Like many other modern proof assistants, Lean uses Type Theory to build its logical formal system, instead of Set Theory.
  • My goal is to show you just enough Type Theory and Lean to make you less scared to act on your curiosity.

Set Theory VS Type Theory (intuition)

Primitives: elements, sets.
Functions are a derived construction.

Primitives: functions, types.
Elements are a derived construction.
Sologan:
  types are like sets that remember their definition.

Type Theory and -calculus

  • -calculus: Old formal system (Church, 1930s). Shifts primitives from sets and elements to functions.
  • The main thing you can do with functions is compose them (into tree-like structures).
  • Type Theory extends -calculus labelling all inputs and outputs with types (like in C++).
  • In well-formed composition trees, all input-output types must match.

Formal foundations: Type Theory

Set Theoretic Formal System

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

Type Theoretic Formal System

  • Type language: term : type, primitive constructions on types
  • E.g., Function Types: func : type1 typen type,
    write application/composition as   func arg1 ... argn
    instead of   func(arg1, ..., argn)

Formal foundations: Type Theory

Translation

  • sets sets are replaced by types, (elem) x (set) X becomes x : X

  • props props are also replaced by types,
    (proof) pf of (prop) P becomes pf : P

  • rules of inference funcs from hypotheses types to conclusion types

  • proof verification type checking: a correct proof is a well-formed tree of composed rules of inference

  • propositional calculus: constructions on proposition types

    • , , are primitives, special cases of
    • , , defined for general (and set-like) types

Formal foundations: Type Theory

rules of inference VS proofs as functions

Formal foundations: Type Theory

rules of inference VS proofs as functions

Formal foundations: Type Theory

rules of inference VS proofs as functions

Formal foundations: Type Theory

rules of inference VS proofs as functions

This well-formed tree is the proof term
   .

Inductive types

Axioms / Recursion / Induction

  • Axioms: Functions declared to exist.
    That may also brings into existence their target Types.
    Ex: : Prop (Prop Prop), or trivial : True
  • Inductive Types:
    • declaring a recursive function(s) fi : T ... T brings into existence
      the inductive type T and an inductive principle for T
    • all terms of T are exhausted by free formal composition of fi
      (well-formed trees with fi nodes)
    • Ex: 0 : , succ : , 1 is succ 0, 2 is succ 1 = succ (succ 0), ...

Dependent types

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
    • Ex: even : Prop, even integers ‘’ = n : (even n)
  • Product type / dependent product: T = b : B (F b) — like the space of sections : B (b : B F b)
    • Ex: proof : ( : Prop) ( : Prop) ... is a dependent function

Quantifiers

  • is a big indexed , is a big indexed .
  • So logical quantifiers are dependent sums / products:
    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
  • Some type constructions must bump up the universe index
  • in Lean Prop : (Type 0), so Prop = (Type ‘-1’)

Lean: first steps

With have enough basic foundation to finally have a look at

  • Lean 4:
    • typed functional programming language (every program is a function)
    • with strong dependent inductive types
    • unicode input (\to => , \pi => , ...), flexible self-defined syntax
    • proof irrelevance, classical logical axioms if needed (Choice, LEM)
    • large growing formalization library Mathlib to build on
  • Installation: git, VS Code/Codium Lean 4 extension
  • Live online: https://live.lean-lang.org/
  • Start learning from Theorem Proving in Lean

Practical demo

Learning Resources

Search and Discovery

Equational project

  • On 25 Sep 2024 Terry Tao announced an online collaborative project: Equational.
  • The goal is to produce a complete (counter-)implication graph for a list of axioms on a set with a single binary operation (a magma as it is known in Universal Algebra).
  • The limitation is to restrict to single-equation axioms, where the binary operation is used at most 4 times: 5000 possibilities
  • Implications / counter-examples are formalized in Lean: anyone can contribute, the correctness of a contribution is verified / certified by Lean.
  • As of 12 Oct 2024 the project is "99.9963%" complete. It is still ongoing due to the stubborn remaining cases.

Shameless Self Promotion

Grant application for BSc/MSc projects (pending for 2025)

Formalize fundamental theorems in Differential Geometry in Lean:

  • Frobenius Theorem (integrable distributions foliations)
  • Stefan-Sussmann Theorem (singular integrable distributions ...)

Columns in Marp: https://github.com/orgs/marp-team/discussions/192