Lean 4 Proof Assistant: Basics, Mathlib, and AI Formalization

What Is Lean

Lean is a functional programming language and an interactive theorem prover (proof assistant). It was started by Leonardo de Moura at Microsoft Research in 2013; the current mainstream version is Lean 4, maintained by the non-profit Lean FRO.

Users write mathematical definitions, theorems, and proofs in Lean. Lean checks each inference step mechanically: if every step follows the rules, the theorem is accepted; otherwise Lean reports an error at the offending location.

Lean's logical foundation is dependent type theory. A core correspondence, "propositions as types", maps each proposition to a type; a proof of the proposition is an element of that type. Verifying a proof thus reduces to type-checking a program, a task computers can perform mechanically.

Basic Syntax

Simplest example:

#eval 2 + 3   -- compute, outputs 5

theorem two_add_three : 2 + 3 = 5 := rfl

theorem

declares a theorem, two_add_three is the name, the colon introduces the proposition, := precedes the proof. rfl (reflexivity) means both sides compute to the same value; Lean computes both sides to 5 and accepts the proof.

If the proposition is false, e.g.: theorem wrong : 2 + 2 = 5 := rfl Lean reports a type error and rejects the theorem.

Proposition with variables: for any natural numbers a b, a + b = b + a.

theorem my_add_comm (a b : Nat) : a + b = b + a := by
  omega

by

enters tactic mode. Tactics are proof-generating commands; omega is Lean's built-in decision procedure for linear arithmetic on integers and naturals.

More complex proofs proceed stepwise. Below, mathematical induction proves 0 + n = n:

theorem zero_add' (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [← Nat.add_assoc, ih]

induction n

performs induction on n. The base case n = 0 holds by computation. In the inductive step, ih is the induction hypothesis 0 + k = k; the goal is 0 + (k + 1) = k + 1. First rewrite using associativity to (0 + k) + 1, then apply ih to get k + 1, matching the right side.

This mirrors paper induction, but every rule application must be explicit; paper proofs' "obviously" or "similarly" must be filled in.

Mathlib

Mathlib is the community-maintained mathematics library covering set theory, algebra, topology, real analysis, number theory, algebraic geometry, etc. Kevin Buzzard estimates the recent Fermat formalization codebase is over five times the size of Mathlib, implying Mathlib is roughly two million lines.

Mathlib's statement of "infinitely many primes":

theorem Nat.exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p

For any natural n, there exists a prime p ≥ n.

Fermat's Last Theorem statement is similarly concise (simplified here, formally different in Mathlib):

∀ a b c n : ℕ, 0 < a → 0 < b → 0 < c → 2 < n → a ^ n + b ^ n ≠ c ^ n

Source of Trustworthiness

The final arbiter in Lean is a tiny program called the kernel. Tactics, automation tools, and external programs (including AI) only produce proof terms; all results must pass the kernel. This design follows the de Bruijn criterion: system trustworthiness rests on a core small enough for human audit.

Therefore, human verification of a Lean proof requires checking only two items:

Whether the theorem statement accurately expresses the intended mathematical proposition.

Which axioms the proof depends on. Lean's standard axioms are three: propositional extensionality ( propext), classical choice ( Classical.choice), and quotient soundness ( Quot.sound). Use #print axioms theorem_name to inspect.

Proof length does not increase human audit effort. This is crucial for AI-generated proofs. Suppose each intermediate lemma has independent error probability p ; the probability that all N lemmas are correct is (1-p)^N . Take p = 0.01 . Even with N = 100 , probability ≈ 0.366; for N = 30000 , probability ≈ 9.3×10⁻¹³⁴. Without mechanical checking, such scale is unverifiable. With a checker, erroneous steps are rejected; the generator can iterate until acceptance, leaving only kernel-verified steps. Recent AI advances in mathematical proof all use Lean as the verification backend: 2024, Google DeepMind's AlphaProof reached IMO silver-medal level; 2025, Harmonic's Aristotle reached IMO gold-medal level. Limitations Formal verification has two classes of limitations. One stems from implementation. In September 2026, security firm Trail of Bits disclosed a Lean 4 bug: the native_decide tactic delegates some computation to compiled code, but a string function's compiled implementation diverged from its logical definition, allowing derivation of a contradiction and thus "proving" any statement, including Fermat's Last Theorem. The bug was fixed within days. Proofs using native_decide show an extra axiom in #print axioms output; auditing the axiom list reveals the issue. The other is fundamental. Lean only checks that the proof derives the written statement; it does not check whether the statement matches the author's intent. A missing hypothesis or a definition diverging from the usual meaning still yields an accepted proof if the derivation is correct. Translating a mathematical claim into an accurate formal statement remains a human responsibility, analogous to the modeling step from real-world problem to mathematical problem. Getting Started Natural Number Game : Browser-based interactive tutorial starting from Peano axioms, proving properties of addition, multiplication, and order. No installation required; middle-school math background suffices. Lean Official Online Editor : Run the examples from this article directly. Local Environment : Install VS Code with the Lean 4 extension. For mathematics, read Mathematics in Lean to learn using Mathlib for university-level math; for language and logic, read Theorem Proving in Lean 4 . Conclusion Regarding this Fermat formalization, Buzzard notes it faithfully follows the early literature's proof without adding new mathematical content; simultaneously, the result demonstrates that research-level mathematics can be formalized concurrently with writing. Formal verification changes how mathematical proofs are confirmed: correctness is mechanically checked by the kernel, while human review focuses on the theorem statement and the axioms used. Whether the statement is correctly written still requires a mathematician's judgment.