Introduction to Lean

Trinh Minh Huy - Vu Quoc Lam - Tu Cong Thanh - Vo Dang Quan

Table of contents

01 02 03
Overview Features Syntax

04 05 06
Execution Model Application Comparison
01
Overview
Motivation - History - Paradigm
What is ?

Lean is an efficient pure functional programming

language and a proof assistant.

Lean is very strongly typed, having an extensible syntax,

and is built for formal mathematics and verification.
What is ?

Lean is an efficient pure functional programming

language and a proof assistant.

Lean is very strongly typed, having an extensible syntax,

and is built for formal mathematics and verification.
What is a proof assistant?

What is wrong with this proof?

What is a proof assistant?
What is a proof assistant?
History of Lean

2013 - 2016 2027-2020 2021-2023 2024-Present

Lean 3 and AI and
Lean 1 and 2 Lean 4
mathlib Modern Era
Highly experimental Lean 3 as stable Complete rewrite into Integration with AI
release, introducing a fast, (AlphaProof), major
tactics and the rise general-purpose math formalizations,
of mathlib language and the and academic
establishment of the awards.
Lean FRO.
Paradigm of

Lean is a pure functional programming language:

● functions are first-class
● data is immutable
● pattern matching and recursion are central
● effects are isolated
Paradigm of

Lean is a pure functional programming language

02
Features
Functional Programming
in Lean
Functional Programming in Lean
• Program behaves like a predictable pipeline.
• Built upon the foundation of lambda calculus, an abstract
mathematical model of computation.
λn.n+1

A Model akin to Mathematics: Example

Currying for Multiple Inputs
• Functions in lambda calculus process exactly one input.
• A multi-input function can be considered a single-input
function that, when supplying an input, returns a new function
waiting for the next input.

λab.a+b ≡ λa.λb.a+b
Looping with Recursion

No traditional Using recursion: a Recursive call Base case is

looping constructs function calling itself represents the “next equivalent to loop
with updated inputs. step”. exit conditions.
Looping with Recursion: Example
 Side Effects: The Problem
Software frequently needs to interact with the outside world (print, read files, network calls).
These interactions—called side effects—break the predictable flow of pure functions.

Impact: External state dependency

Example: IO operation
Side effects make behavior harder because
(e.g. printing to console, read a file)
the function's outcome depends on and
modifies external state.
 Side Effects: State Passing for Purity
To maintain mathematical purity, functions receive the "external state"
as an input parameter and return an updated "external state" as an
output.
Side effect: Manual Plumbing
Threading the world token everywhere quickly becomes tedious
and error-prone:

Boilerplate More bugs

Passing the Reusing an
"external state" outdated "external
through every state"
single function
Introducing Monads: The Mechanics

Return value
Instead of manually taking and returning world
state, our functions simply return an IO value.

Bind operators
Use bind operator to unpack the result, handles
the state update behind the scenes, and feeds the
value forward.
Introducing monads: Example
do-Notation for Ergonomic
• do-notation: syntax sugar that translates
imperative-looking code into pure chains of bind calls.
`do` notation: Another example
Lean as a
Proof Assistant
Lean is Strongly Typed
Values have types.

…How is this relevant?

Logical Intepretation of Program
• Deep connection between formal logic and computation,
known as Curry-Howard correspondence.
• Programs posses a logical intepretation:

Logic Programming

Proposition Type

Proof Term

• Proving a proposition is the same as computing a term

for a type.
Type universe
• In Lean, every expression has a type, and even types
themselves has types, called type universes.
• To avoid logical paradoxes, Lean uses an infinite hierarchy:
Sort 0 Sort 1 Sort 2 ...
(or Prop) (or Type)
The universe of The universe of The universe of
logical propositions computational data generic structures

• Types in Lean can act just like values; it can be used in

most places values are.
Truth and Falsehood
• A proposition is true if its
corresponding type has at
least a value, and false
otherwise.

• True is a type with exactly

one constructor.
• False is a type with zero
constructors.
 Function v.s. Implication

f: P → Q P⇒Q
Input type P to output type Q P is true then Q is true

Function represents Implication

Using Implication in Proof
Logical connectives
In Lean, standard logical operators are represented as type
constructors, which are functions over types.
Concepts Notation Type Code

Conjunction P⋀Q And

Disjunction P⋁Q Or

Negation ¬P Not
Predicate
• A predicate is a logical statement that depends on a value.
• Lean models this using function returning types.

Predicate as Lean type

Universal Quantification — ∀
Lean models
this using a
dependent
function,
where the
output type
depends on
the input.
Existential Quantification — Ǝ
Lean simply represents this with a dependent pair: a specific
value, and a proof of the predicate in question.

Existential Quantification as Lean type

Inductive proof in Lean
• Inductive definition allow Lean to define and reason over
infinite domain (such as natural number).
• Because inductive type are naturally recursive, a
recursive function is naturally a proof by induction.

Natural Number’s Definition

Proof by Induction
Summary
• Curry-Howard correspondence allow programs to
represent logic.
• Key idea: proposition-as-type, proof-as-term.
• Lean's formal logic foundation is the Calculus of Inductive
Constructions (CIC), combining the usual type systems with
dependent type, as well as inductive definition.
Proving in Lean: Summary
Tactics in
Lean proofs are terms, but tactics give a more incremental
way to build those terms.

Without tactic:

With tactic:
Tactics in
Lean proofs are terms, but tactics give a more incremental
way to build those terms.
With tactic: Natural deduction:
 Tactics in
Tactic mode with by, and by can appear anywhere a term is
expected.
Tactics run top to bottom, each updating the current proof state.
 Tactics in
rfl (reflexitivity tactic) closes a goal when both sides are
definitionally the same.
 Tactics in
rw rewrites a goal or hypothesis using a chosen equality. Then
Lean closes the reflexive equality automatically.

● a=b
● a+1=b+1
● b+1=b+1
 Tactics in
simp repeatedly simplifies an expression using lemmas marked
[simp] and any extra facts you provide.
Tactics in

intro assumption induction cases

exists contradiction show have

exact constructor apply <;>

 Tactics in
bv_decide reduces the problem to SAT, lets a high-performance
solver search, and then checks the returned certificate inside Lean.
 Tactics in
omega implements a variant of Cooper's algorithm.
Specialized arithmetic tactic. Works on Nat, Int, Fin, UInt, BitVec.
 Tactics in
grind is broad automation inspired by
SMT solvers.
● Discovers new equalities, ineqs,...
● Writes facts on the board and
merges equivalent terms
● Multiple engines cooperate on the
same workspace: Congruence
closure, E-matching, Constraint
propagation, Guided case analysis
Tactics in
Mathlib: The Ecosystem Engine
Mathlib is the largest community-build
library of formalized mathematics.

Mathlib is a foundational infrastructure

for formal mathematics, enabling both
frontier research and real-world
verification.

Scale Reliability Impact

 Mathlib: The Ecosystem Engine

> 2,000,000 500+

Lines of Contributors

Code

Researchers now don’t start from scratch,

They build upn a massive, reusable base of
theorems.
03
Syntax
 Keywords
Lean do not have a static grammar or syntax because Lean’s syntax is extensible
and any library or packages can extend their custom syntax and rules

Category Count Examples

Core declarations and term syntax 80 def, theorem, structure,
inductive, if, open

Interactive inspection and evaluation 13 #check, #eval, #print

Refine declarations and parser 30 true, false, rec, priority

behavior

Internal / parser-construction tokens 31 leading_parser, private_decl%,

decl_name%
ID Naming Rule
• Prefix: Starts with an alphabetic
character, _, or a Unicode letter-like
symbol.
• Suffix: Can include digits, '
(apostrophe), !, ?, and subscripts.
• Namespaces: Identifiers can be
dotted (e.g., [Link] has two
components).
• Escaping: Surrounded by double
guillemets (« »). Can contain any
character
(e.g., «if», «Đây là một biến»). Note: «x»
and x denote the exact same identifier.
ID Naming Rule
[\a_\l][\a\d_!?'\l\s]*(.[\a_\l][\a\d_!?'\l\s]*)*

● \a: Alphabetic character

● \l: Letter-like symbol
● \d: Any digit (0-9)
● \s: Subscript
ID Naming Rule
[\a_\l][\a\d_!?'\l\s]*(.[\a_\l][\a\d_!?'\l\s]*)*

α β₁ x _tmp1 [Link]

done! ok? «if» «Đây là một biến» x'

 Numerical Syntaxes
Decimal [0-9](?:[0-9_]*[0-9])?

Some examples:
0, 7, 1_000
 Numerical Syntaxes
Octal 0[oO][0-7](?:[0-7_]*[0-7])?

Some examples:
0o7, 0O755, 0o1_2_3
 Numerical Syntaxes
Hexadecimal 0[xX][0-9A-Fa-f](?:[0-9A-Fa-f_]*[0-9A-Fa-f])?

Some examples:
0x0, 0xFF, 0Xdead_beef
 Numerical Syntaxes
Binary 0[bB][01](?:[01_]*[01])?

Some examples:
0b1, 0B1010, 0b10_01
 Numerical Syntaxes
Scientific (?:\d+(?:\.\d*)?|\.\d+)(?:[eE][+-]?\d+)?

Some examples:
1.0, 1., 12e3, 1.2e+5
 Whitespace & Comment

Block Comments: /-
Line Comments: denoted opens, -/ closes. Block
by --, all subsequent comments can be nested
characters on the line act
as whitespaces

Documentation: /-- or,

/-! Generate formal doc
string

Whitespace: Lean tokens are

separated by spaces. Lean
treats tabs, newlines and
comments to be whitespaces
Definition
 def add1(n : Nat) : Nat := n + 1

● <name> : the identifier of the function

● <parameter> : inputs, bounded with
open/close bracket
● <type> : returned type
● <term> : details of the function
 Extensible Syntax
● makes code easier to read
Lean lets you define new syntax so
● helps create small domain-specific
code can look closer to the math or
languages
language you want.
● lets libraries feel natural to use
04
Execution Model
Pipeline - Elaboration - Compilation
Pipeline of

Main stages:
● Parsing
● Macro Expansion
● Elaboration
● Kernel Checking
● Compilation
Pipeline of
Pipeline of
programmable!
Pipeline of
Pipeline of
Extensibility of
Extensibility of
05
Application
Growth & Adoption

90,000+
Since beginning of 2024

17,000+
Over Q4 2025

+21%
Increase over Q3
Growth & Adoption

90,000+
Since beginning of 2024

17,000+
Over Q4 2025

+21%
Increase over Q3
Main Application

Formal Mathematics Software & Security System Verification

Focus Focus Focus

Proving theorem with Ensuring mission-critical Verifying safe system code
machine-checked certainty. systems and policies behave beyond basic memory safety.
flawlessly.
Key Projects Key Projects
The Liquid Tensor Equipment, Key Projects Aeneas (tooling for
Polynomial Freiman-Ruzza CSLin is a computer science translating Rust programs
conjecture. equivalent to Mathlib. directly to Lean proofs).
[Link]/pdf/[Link]
[Link]/pdf/[Link]
Main Application

Formal Mathematics Software & Security System Verification

Focus Focus Focus

Proving theorem with Ensuring mission-critical Verifying safe system code
machine-checked certainty. systems and policies behave beyond basic memory safety.
flawlessly.
Key Projects Key Projects
The Liquid Tensor Equipment, Key Projects Aeneas (tooling for
Polynomial Freiman-Ruzza CSLin is a computer science translating Rust programs
conjecture. equivalent to Mathlib. directly to Lean proofs).
 Who are using Lean
Industry

AI Start-ups

Academia
 Verification Tools

AI systems excel at generating code. But can you trust that code? Lean provides the missing piece:
proof that the code is correct.

Velvet: mvcgen
Imperative program verifier (Oct 2025) Lean FRO's monadic verification framework

Aeneas
Strata
Rust verification via translation to Lean
A unified platform for formalizing language
syntax and semantics
Main Application

Formal Mathematics Software & Security System Verification

Focus Focus Focus

Proving theorem with Ensuring mission-critical Verifying safe system code
machine-checked certainty. systems and policies behave beyond basic memory safety.
flawlessly.
Key Projects Key Projects
The Liquid Tensor Equipment, Key Projects Aeneas (tooling for
Polynomial Freiman-Ruzza CSLin is a computer science translating Rust programs
conjecture. equivalent to Mathlib. directly to Lean proofs).
AI Connection - Training on Truth
AI Connection - Training on Truth
06
Comparison
 Prover & Prover & Purely General
Role
Language Language Functional PL Scripting PL

Type system CIC CIC Static Typed Dynamic Typed

Transpiled to Compiled /
Execution Transpiled to C Interpreted
OCaml Interpreted

Formal math, Formal specs, Pure function,

Sweet spot verification, Certified Typed Science, AI
general coding extraction abstractions
Thanks!
Do you have any questions?

CREDITS: This presentation template was created by

Slidesgo, including icons by Flaticon, and infographics
& images by Freepik

Please keep this slide as attribution