Lean: Machine Verified Mathematics

A programming language and proof assistant for Mathematicians.

Anirudh Gupta · IISc Bengaluru

Madhava Mathematics Nurture Camp · 2026

B.K. Birla College, Kalyan

anirudhgupta@iisc.ac.in · GitHub

How do we know a proof is correct?

For every great theorem proved, Mathematicians sit together and verify that yes the proof is correct.

This has been the classic way of checking and verifying Mathematics.

So What's the problem? All good right?

Modern proofs are huge: the classification of finite simple groups runs to tens of thousands of pages.

How do you know mathematicians didn't skip any case? Apart from Trusting them of course.

The worry: Can we trust a proof which is a 100 pages long, took a decade to "solve" and checked by humans which, though smart, can't remember what they had for breakfast last week.

The idea

Write mathematics in a language a computer can read.

Let it check every single step — down to the axioms. No hand-waving, no "clearly", no gaps.

If it is accepted, it is correct — as correct as the tiny trusted core that checks it.

Formal mathematics: proofs written so precisely that a machine can verify them.

So — what is Lean?

Lean is two things at once:

a real programming language — you can compute with it, and

an interactive theorem prover — you can prove theorems in it.

Created by Leonardo de Moura (2013 →), now developed by the Lean FRO and a large open community.

The same language runs your code and checks your proofs. That is the whole trick.

How Lean impacts Mathematics Today?

"Lean enables large-scale collaboration by allowing mathematicians to break down complex proofs into smaller, verifiable components. This formalization process ensures the correctness of proofs and facilitates contributions from a broader community. With Lean, we are beginning to see how AI can accelerate the formalization of mathematics, opening up new possibilities for research." — Terence Tao

Lean and Mathlib are used at the frontier of mathematics:

the Liquid Tensor Experiment — Peter Scholze asked for a formal check of a hard theorem; it was completed.

Fermat's Last Theorem — a large ongoing formalization project.

Terence Tao and others now formalize new results as they publish.

AI systems learn to prove theorems in Lean, with the checker keeping them honest.

and many more...

Part I · Lean computes

Computation comes to mathematics

Lean is a programming language

A functional Programming Language at it's core, following mathematical principles for construction.

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

#eval55 fib 10                       -- 55
55
#eval[1, 4, 9, 16, 25] [1, 2, 3, 4, 5].map (· ^ 2)  -- [1, 4, 9, 16, 25]
[1, 4, 9, 16, 25]

Computation is checked too — the types guarantee fib returns a Nat.

Part II · Lean proves

From computation to certainty

All defintions in Lean, are defined the classical way Mathematics defines them.

inductive Nat' where
  /- Zero, the smallest natural number. -/
  | zero : Nat'
  /- The successor of a natural number `n` -/
  | succ (n : Nat') : Nat'

Some Theorems on Nat from Source code:

@[simp] theorem add_eq : Nat.add x y = x + y := rfl
theorem add_right_cancel {n m k : Nat} (h : n + m = k + m)
    : n = k := byn:Natm:Natk:Nath:n + m = k + m⊢ n = k
  rw [Nat.add_comm n m,n:Natm:Natk:Nath:m + n = k + m⊢ n = k Nat.add_comm k mn:Natm:Natk:Nath:m + n = m + k⊢ n = k] at hn:Natm:Natk:Nath:m + n = m + k⊢ n = k
  apply Nat.add_left_cancel hAll goals completed! 🐙

A theorem, checked line by line

Lean has inbuilt theorem prover, powerful automation as tactics to check correctness and help you prove your theorem.

-- Fibonacci never decreases
theorem fib_monotonic (n : Nat) : fib n ≤ fib (n + 1) := byn:Nat⊢ fib n ≤ fib (n + 1)
  induction n with
  | zero =>zero⊢ fib 0 ≤ fib (0 + 1) decideAll goals completed! 🐙   -- fib 0 = 0 ≤ fib 1 = 1
  | succ n ih =>succn:Natih:fib n ≤ fib (n + 1)⊢ fib (n + 1) ≤ fib (n + 1 + 1)
    -- goal: fib (n + 1) ≤ fib (n + 2)
    -- grind [fib]
    have hf: fib (n + 1) ≤ fib (n + 2) := byn:Nat⊢ fib n ≤ fib (n + 1)
      calc fib (n + 1) ≤ fib n + fib (n + 1) :=
        Nat.le_add_left _ _
        _ = fib (n + 2) := rflsuccn:Natih:fib n ≤ fib (n + 1)hf:fib (n + 1) ≤ fib (n + 2)⊢ fib (n + 1) ≤ fib (n + 1 + 1)
    assumptionAll goals completed! 🐙

/-- Addition is commutative on Naturals -/
theorem add_comm (a b : Nat) : a + b = b + a := bya:Natb:Nat⊢ a + b = b + a
  induction b with
  | zero =>zeroa:Nat⊢ a + 0 = 0 + a simp only [Nat.add_zero, Nat.zero_add]All goals completed! 🐙
  | succ n ih =>succa:Natn:Natih:a + n = n + a⊢ a + (n + 1) = n + 1 + a rw [Nat.add_succ,succa:Natn:Natih:a + n = n + a⊢ (a + n).succ = n + 1 + a ih,succa:Natn:Natih:a + n = n + a⊢ (n + a).succ = n + 1 + a Nat.succ_addsucca:Natn:Natih:a + n = n + a⊢ (n + a).succ = (n + a).succ]All goals completed! 🐙

Each tactic (induction, simp, rw, grind) is a checked step. Lean refuses to accept a proof with a gap.

Proofs are programs

A deep idea Lean is built on: a proposition is a type, and a proof is a term of that type.

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := byp:Propq:Prophp:phq:q⊢ p ∧ q
  constructorleftp:Propq:Prophp:phq:q⊢ prightp:Propq:Prophp:phq:q⊢ q      -- goal splits into ⊢ p and ⊢ q
  ·leftp:Propq:Prophp:phq:q⊢ p exact hpAll goals completed! 🐙
  ·rightp:Propq:Prophp:phq:q⊢ q exact hqAll goals completed! 🐙

-- "p and q implies q and p" — the proof is just a function.
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
  fun h => ⟨h.right, h.left⟩

Curry–Howard: proving and programming are the same activity.

It is interactive

You do not write the whole proof at once. You build it step by step, and Lean shows you the goal that remains:

/-- Sum of two naturals -/
def sum : Nat → Nat
  | 0 => 0
  | n + 1 => n + 1 + sum n

/- Proving sum of first n natural numbers -/
theorem sum_formula (n: Nat) :
  2 * sum n = (n * (n + 1) ) := byn:Nat⊢ 2 * sum n = n * (n + 1)
  induction n with
  | zero =>zero⊢ 2 * sum 0 = 0 * (0 + 1) rflAll goals completed! 🐙
  | succ n ih =>succn:Natih:2 * sum n = n * (n + 1)⊢ 2 * sum (n + 1) = (n + 1) * (n + 1 + 1)
      unfold sumsuccn:Natih:2 * sum n = n * (n + 1)⊢ 2 * (n + 1 + sum n) = (n + 1) * (n + 1 + 1)
      grind [sum]All goals completed! 🐙

The editor's Infoview shows the live goal state at your cursor — proving becomes a conversation.

Flags proofs when theorem is wrong

A system which doesn't let you prove if something is wrong!

/- Successor function -/
def succFn (n : Nat) : Nat := n + 1

/- Successor is Surjective. But this is wrong! -/
theorem succFn_surjective : ∀ y, ∃ x, succFn x = y := by⊢ ∀ (y : Nat), ∃ x, succFn x = y
  intro yy:Nat⊢ ∃ x, succFn x = y
  unfold succFny:Nat⊢ ∃ x, x + 1 = y
  omegaAll goals completed! 🐙omega could not prove the goal:
No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.

y = 0 has no preimage — no x with x + 1 = 0. The claim was false, and Lean simply won't fake a proof of it.

...the actual truth, proved

succFn really is injective — it's just not surjective too. Two separate, both TRUE, both provable:

theorem succFn_injective (a b : Nat)
  (h : succFn a = succFn b) : a = b := bya:Natb:Nath:succFn a = succFn b⊢ a = b
  unfold succFn at ha:Natb:Nath:a + 1 = b + 1⊢ a = b
  omegaAll goals completed! 🐙

theorem succFn_not_surjective : ¬ (∀ y, ∃ x, succFn x = y)
    := by⊢ ¬∀ (y : Nat), ∃ x, succFn x = y
  intro hh:∀ (y : Nat), ∃ x, succFn x = y⊢ False
  obtain ⟨x, hx⟩ := h 0h:∀ (y : Nat), ∃ x, succFn x = yx:Nathx:succFn x = 0⊢ False
  unfold succFn at hxh:∀ (y : Nat), ∃ x, succFn x = yx:Nathx:x + 1 = 0⊢ False
  omegaAll goals completed! 🐙

Injective and surjective are genuinely different — even for something this simple. Lean won't let you blur that.

Mathlib - Mathematics Library of Lean

A shared, machine-checked library of mathematics

Mathlib is a single, unified library of formalized mathematics:

over 1.5 million lines, thousands of contributors

groups, rings, fields · analysis and limits · topology · measure theory · number theory · category theory · manifolds …

every result checked, and reused — you build on what is already there.

Most undergraduate mathematics has been proved. Lots of researches have been proved too.

Prove your lemma once, correctly, and everyone can trust and reuse it.

Lean in the World

Terence Tao on Lean

Startups in Lean

Why should you care?

Lean is become a well-recognized and accepted method for formalizing proofs for correctness.

No gaps. The computer will not let you skip a step — great for learning.

Instant feedback. Try an idea, see immediately if it holds.

Collaboration. Build on a shared, trusted library.

AI + Lean. Automated proving and autoformalization are moving fast — and Lean is where it happens.

In the age of computing and AI, Professors around the world encourage everyone to Learn Lean to adapt to this new age.

Live demo

Let's open the editor

Live-Lean Demo Code(Click me)

Getting started

Everything is free and open:

Natural Number Game — prove theorems in your browser, no install.

Mathematics in Lean — the standard tutorial book.

live.lean-lang.org — try Lean online, Mathlib included.

The Lean Zulip chat — a famously welcoming community.

leanprover-community.github.io · lean-lang.org

Thank you

Questions?

GitHub · anirudhgupta@iisc.ac.in