Lean: Machine Checked Mathematics and Software

A programming language and proof assistant for Mathematics and Software Verification.

Anirudh Gupta · IISc Bengaluru

B.K. Birla College, Kalyan

Science is increasingly interdisciplinary

Modern breakthroughs rarely stay inside one department.
Biology now depends on computation, statistics, and learning systems.
The most important tools often live between fields, not inside one.

Demis Hassabis: With knowledge of AI, neuroscience, and biology which he put together, he made AlphaFold, which helped earn the 2024 Nobel Prize in Chemistry.

When the problem spans fields, the language of trust should span fields too.

Mathematics, Computer Science and Today

Mathematics

Computer Science

Lean

The power that Mathematics is in Theorems. So why not use it?

What Lean gives you

A programming language for computation.

An interactive theorem prover for proofs.

A shared environment where the same file can run code and verify claims.

#eval is a discovery tool too — compute examples first, then conjecture and prove.

def listSearch? (xs : List Nat) (y : Nat) : Nat :=
  match xs with
  | [] => 0
  | x :: xs' => if x = y then 0 else 1 + listSearch? xs' y

-- The SAME file that runs this can prove a fact about it:
theorem listSearch?_head (xs : List Nat) (y : Nat) :
    listSearch? (y :: xs) y = 0 := byxs:List Naty:Nat⊢ listSearch? (y :: xs) y = 0
  simp [listSearch?]All goals completed! 🐙

The core idea

Lean turns specifications into code that can be verified mathematically.
A proof of correctness is a guarantee that the code meets the specification.

Mindset Shift

From asking whether a program looks correct → Proving that it is correct.

"But who checks the checker?" — a small, human-auditable kernel does. Trust it once, and every proof it accepts is correct.

Idea

→

Lean code

→

Proof of correctness

The proof assistant is the judge. If it tells you the proof is valid, you can trust the math.

Paradigms for Software Testing

Tests sample behavior. Proofs certify behavior.

Tests are finite; bugs live in infinite input spaces.

A passing test suite is evidence, not a guarantee.

Proofs force you to state the property for every input that matches the specification.

If the specification is wrong, tests may never notice. A proof attempt usually forces the mistake into the open.

A bug that tests can miss

def binarysearch(a, x):
  lo, hi = 0, len(a)
  while lo < hi:
    mid = (lo + hi) // 2
    if a[mid] < x:
      lo = mid    # bug: should be mid + 1
    else:
      hi = mid
  return lo

Most test inputs never land on the one case that breaks: hi - lo = 1. A proof has to face it anyway.

The same bug, formalized

The bound update, distilled to just the arithmetic — same mistake, no array required:

def lowerUpdate (lo hi : Nat) : Nat :=
  (lo + hi) / 2          -- bug: same mistake as the Python

The range must shrink every step, or the search never ends. Let's ask Lean to check that:

theorem lowerUpdate_progress (lo hi : Nat) (_h : lo < hi) :
    lo < lowerUpdate lo hi := bylo:Nathi:Nat_h:lo < hi⊢ lo < lowerUpdate lo hi
  unfold lowerUpdatelo:Nathi:Nat_h:lo < hi⊢ lo < (lo + hi) / 2
  omegaAll goals completed! 🐙omega could not prove the goal:
a possible counterexample may satisfy the constraints
  b ≥ 0
  b - c ≥ 0
  a ≥ 0
  a - b ≥ 1
  0 ≤ a + b - 2*c ≤ 1
where
 a := ↑hi
 b := ↑lo
 c := ↑(lo + hi) / 2

lo = 0, hi = 1 breaks it: lowerUpdate 0 1 = 0, so lo < lowerUpdate lo hi is just false. Lean refuses to fake a proof of a false statement — that refusal is the bug report.

...and fixed

One token — + 1 — is the entire fix:

def lowerUpdate' (lo hi : Nat) : Nat :=
  (lo + hi) / 2 + 1

theorem lowerUpdate_progress' (lo hi : Nat) (h : lo < hi) :
    lo < lowerUpdate' lo hi := bylo:Nathi:Nath:lo < hi⊢ lo < lowerUpdate' lo hi
  unfold lowerUpdate'lo:Nathi:Nath:lo < hi⊢ lo < (lo + hi) / 2 + 1
  grindAll goals completed! 🐙

Testing finds examples. Proving eliminates whole classes of failures.

Lean in the world

Lean is used by Mathematicians, Computer Scientists and today, even in industry, for Software Testing.

MathematicsMathlib1M+ lines, ~400 contributors — one shared, growing library for all of formalized mathematics.

MathematicsLiquid Tensor ExperimentPeter Scholze publicly doubted his own proof was airtight; Lean checked it in months.

MathematicsPFR conjecture, 2023Terence Tao's team formalized a brand-new, unpublished result — proof and formalization almost side by side.

EducationThe Xena ProjectKevin Buzzard teaches undergraduates at Imperial College by having them formalize their own coursework in Lean.

SoftwareIndustry verificationTeams in security, crypto, infrastructure, and large research labs use theorem proving and formal methods to reduce risk.

Lean matters because it scales from student proofs to serious verification work — and from a Fields Medalist's private worry to a first-year's homework.

When bugs are expensive, proofs are cheaper than incidents. When a proof is contested, Lean settles it.

Lean and Games

Lean Theorems are proved using tactics. These tactics are like moves in a game, and the proof is a winning strategy. Watch the goal change after every move:

theorem length_append : ∀ (xs ys : List Nat),
    (xs ++ ys).length = xs.length + ys.length := by⊢ ∀ (xs ys : List Nat), (xs ++ ys).length = xs.length + ys.length
  intro xs ysxs:List Natys:List Nat⊢ (xs ++ ys).length = xs.length + ys.length
  induction xs with
  | nil =>nilys:List Nat⊢ ([] ++ ys).length = [].length + ys.length simpAll goals completed! 🐙
  | cons x xs ih =>consys:List Natx:Natxs:List Natih:(xs ++ ys).length = xs.length + ys.length⊢ (x :: xs ++ ys).length = (x :: xs).length + ys.length
    simp only [List.cons_append, List.length_cons]consys:List Natx:Natxs:List Natih:(xs ++ ys).length = xs.length + ys.length⊢ (xs ++ ys).length + 1 = xs.length + 1 + ys.length
    omegaAll goals completed! 🐙

The ability to make a game out of a proof, turning mathematics into a game, is a powerful!

Who can play this game?

Your Pet. Why not??

AI. Lean is a referee that can check every step.

As long as you can write a tactic, know a little bit of math and coding, you can play this game. You can DO Mathematics in a way you have never done before.

AI in Lean

AI can learn to play the game of proving theorems in Lean.
The Lean checks each steps, tells AI if it is valid or not.
Now AI systems can prove mathematical and software correctness theorems, with Lean as the referee.

Autoformalization is the future of mathematics and software verification.

Vibe Proving

"Vibe coding" — let an AI write code you don't fully check — is fine until the bug is expensive. Vibe proving is the fix: let AI attempt the proof, and let Lean be the one that actually checks it.

Vibe proving examples