• This repository
• Lean 4
  • Brief history
  • Description
  • "Basic" libraries
  • Resources

This repository

This repository contains material for the anzenlang Lean 4 introduction course. It is released under the Mozilla Public License v2.0, see LICENSE for more details.

Participants learn Lean 4 by writing an interpreter for (an extended version of) the [brainfuck] language. The material is not self-sufficient to properly present Lean 4, it requires a trainer guiding participants and presenting/adding context to every step of the process.

See resources for standalone Lean 4 learning material, in particular Functional Programming in Lean.

Lean 4

• Lean 4 on wikipedia

Brief history

• 2013: Leonardo de Moura "releases" Lean 1

  compiler mostly in C++

• 2017: Lean 3, first "stable" version, still (very) experimental

  compiler still mostly C++

• 2021: Lean 4, first stable version

  compiler (eventually) almost completely written in Lean 4

• 2023: creation of the Lean FRO to improve Lean 4 scalability and usability

Description

• terminating, purely functional language

• strong, dependent type system

• great development language, also a great Interactive Theorem Prover (ITP)

• heavily inspired by ML, Coq, and Haskell

• modern: (Rust-)cargo-like environment, utf-8-friendly, extremely clean syntax

  • elan: toolchain manager, fork of Rust's rustup
  • lake: project manager, pure Lean but based on Rust's cargo

• efficient

  • compiles to C
  • very clever reference-counting-like memory management

"Basic" libraries

The Lean 4 community provides three "basic" packages/libraries:

• core: historically, contained only what the Lean compiler needs

  now transitioning to being a minimal standard library

  https://github.com/leanprover/lean4

• batteries (formerly std/std4): development-oriented standard library

  augments core with bells and whistles

  https://github.com/leanprover/std4

• mathlib4/mathlib: ITP standard library

  augments core and batteries with mostly theoretical definitions

  results from algebra, category theory, ...

  https://github.com/leanprover-community/mathlib4

Documentation for these libraries available here:

• https://leanprover-community.github.io/mathlib4_docs

Resources

• API documentation: https://leanprover-community.github.io/mathlib4_docs

• homepage

• Lean FRO

• community website, aggregates many resources including Lean's Zulip

• lake documentation, the Lean project manager

• doc-gen4, Lean project documentation generation

Learning:

• Functional Programming in Lean (FPiL)

  https://lean-lang.org/functional_programming_in_lean/

• Theorem-Proving in Lean (TPiL)

  https://lean-lang.org/theorem_proving_in_lean4/

• Meta-Programming in Lean (MPiL)

  https://leanprover-community.github.io/lean4-metaprogramming-book/

• Lean manual

  https://lean-lang.org/lean4/doc/

• Mathematics in Lean

  https://leanprover-community.github.io/mathematics_in_lean/index.html

• Logic and mechanized reasoning

  https://avigad.github.io/lamr/index.html

• Lean game server: game-ified resources for the ITP part of Lean 4

  https://adam.math.hhu.de