Lean Programming Language
Lean, more accurately written Lean rather than LEAN, is a programming language designed for exact reasoning. It is not only a language in which we can write programs. It is also a proof assistant, meaning a system in which we can write mathematical statements and then construct proofs that are checked by the computer. The official Lean website describes Lean as an open-source programming language and proof assistant for correct, maintainable, and formally verified code, while the official learning page describes it as a functional programming language and theorem prover for formalizing mathematics, formal verification, and general coding.
The simplest way to understand Lean is to begin from a familiar question. In ordinary programming, when we write a function, the compiler checks whether the function is syntactically legal and whether the types are compatible. If a function expects a natural number, the language should not silently treat a string as a natural number. Lean does this kind of checking too, but it goes further. Lean can also check whether a mathematical proof is correct. This makes Lean a bridge between programming and mathematics.
In Python, JavaScript, C, or C++, we usually ask, “Does this program run?” In Lean, we can ask a stronger question: “Can I prove that this program, theorem, or definition has the property I claim?” That is why Lean is useful in formal mathematics, verified software, programming-language theory, hardware verification, and AI-assisted mathematics.
Programs, Types, and Exact Meaning
Let us begin with Lean as an ordinary functional programming language. A small Lean program looks like this:
def double (n : Nat) : Nat :=
n + n
#eval double 5
The expression n : Nat means that n has type Nat, where Nat is the type of natural numbers. The expression after the colon in the function header tells Lean the output type. So the line
def double (n : Nat) : Nat :=
means: define a function called double; it takes an input n, where n is a natural number; it returns a natural number. The body of the function is n + n. The command #eval double 5 asks Lean to evaluate the expression.
This already shows one important idea: Lean tries to make meaning explicit. In informal mathematics, we often rely on context. In Lean, the context must be encoded. If an object is a natural number, a proposition, a function, a group, a vector space, or a proof, Lean wants to know that explicitly or infer it from the surrounding code.
Lean as a Theorem Prover
Lean becomes especially powerful when we use it to prove theorems. Consider the following example:
theorem two_plus_two : 2 + 2 = 4 := by
rfl
This defines a theorem named two_plus_two. The statement of the theorem is 2 + 2 = 4. The proof is given after := by. The tactic rfl means reflexivity1.1. Here Lean can reduce 2 + 2 to 4, so both sides are definitionally the same, and the proof is accepted.
A more general example is:
theorem add_zero_right (n : Nat) : n + 0 = n := by
exact Nat.add_zero n
This theorem says that for every natural number n, adding zero on the right gives back n. The phrase Nat.add_zero n refers to an existing theorem about natural numbers. The command exact tells Lean: the object I am giving you is exactly the proof required for the current goal.
The important point is that a Lean theorem is not merely a sentence printed in a document. It is a formal object checked by Lean’s kernel. If Lean accepts the theorem without unproven assumptions such as sorry or extra axioms, then the proof has passed the formal rules of Lean’s underlying logic.
The Central Principle: Propositions as Types
The deep idea behind Lean is often summarized by the phrase propositions as types. In ordinary mathematics, we think of a proposition as a statement that may be true or false. In Lean, a proposition is treated as a type, and a proof of that proposition is treated as a term inhabiting that type.
For example:
example (P Q : Prop) (hP : P) (hPQ : P -> Q) : Q := by
exact hPQ hP
This says: let P and Q be propositions. Suppose hP is a proof of P, and suppose hPQ is a proof of P -> Q, meaning a function that turns a proof of P into a proof of Q. Then hPQ hP is a proof of Q.
This is why Lean can unify programming and proving. A function has an input type and an output type. A proof of implication also behaves like a function: if you give it a proof of the premise, it returns a proof of the conclusion. Therefore, proving becomes a special kind of programming, and programming becomes something that can be reasoned about inside the same language.
Dependent Types
Lean is not merely typed; it is dependently typed. In many programming languages, types classify values. For example, 5 has type Nat, true has type Bool, and a text string has type String. This is already useful, because it prevents many meaningless operations.
Dependent types go further: types may depend on values. For example, one may represent “a list of integers whose length is exactly three” as a different type from “a list of integers whose length is exactly four.” In ordinary programming, the length condition is often checked at runtime. In a dependently typed setting, the length condition can be made part of the type itself.
This matters because mathematics is full of value-dependent constraints. A matrix has dimensions. A vector space has a field. A finite set has a cardinality. A probability distribution has a normalization condition. A unitary matrix must satisfy a preservation law. Lean’s type system gives us a way to express such structures more precisely than ordinary programming languages usually allow.
For example, in a quantum-information context, a human may write, “Let \(U\) be a unitary operator.” In Lean, one should not merely write a matrix and hope it is unitary. One should encode the structure or assumption that makes U unitary. Once that is done, later theorems can require the unitary property explicitly, and Lean will force the proof to supply it.
Tactics: Human-Friendly Proof Construction
Lean proofs can be written as direct proof terms, but many Lean proofs are written using tactics. A tactic is a command that transforms the current proof goal into simpler goals.
For example:
example (P Q : Prop) : P -> Q -> P := by
intro hP
intro hQ
exact hP
The theorem says: if P is true, and if Q is true, then P is true. The tactic intro hP introduces the first assumption and names it hP. The tactic intro hQ introduces the second assumption and names it hQ. The command exact hP completes the proof because the goal is to prove P, and hP is already a proof of P.
Some common Lean tactics are intro, exact, apply, rw, simp, rfl, and induction. The tactic rw rewrites using an equality. The tactic simp simplifies expressions using known simplification rules. The tactic induction proves a statement by induction. These tactics make Lean more usable for humans, because writing raw proof terms for large theorems would often be painful.
Still, tactics are not magic. A tactic may search, simplify, rewrite, or construct a proof, but the result must still be accepted by Lean’s kernel. This is crucial. Lean’s trust does not come from believing that every tactic is correct. It comes from checking the formal proof object produced at the end.
The Kernel: Why Lean Proofs Are Trustworthy
Lean has many convenient layers: notation, elaboration, type-class inference, tactics, automation, macros, and libraries. These layers help humans write proofs in a readable way. But the most trusted part is smaller: the kernel. The kernel checks the final elaborated proof term against the rules of Lean’s type theory.
This architecture is one reason proof assistants are valuable. If a high-level tactic has a bug but produces an invalid proof term, the kernel should reject it. In this sense, Lean separates convenience from trust. The outer language is expressive and automated; the inner checker is stricter.
There are caveats. If a theorem uses sorry, Lean treats the proof as intentionally omitted. If a theorem depends on an axiom, then the theorem is only as trustworthy as that axiom and its consistency with the rest of the system. Lean’s reference manual explicitly warns that axioms must be used with care because inconsistent or false axioms can undermine proofs.
So Lean gives machine-checked correctness relative to the formal statement and assumptions. It does not automatically guarantee that the formal statement perfectly captures the informal scientific or engineering problem. The human still has to formalize the right thing.
Mathlib: The Library of Formalized Mathematics
Lean by itself is already a proof assistant and programming language, but much of its mathematical power comes from mathlib, the community library of formalized mathematics. Mathlib provides definitions, theorems, tactics, algebraic hierarchies, topological structures, order theory, analysis, linear algebra, category theory, and many other topics.
This is important because formal mathematics is cumulative. Once a theorem is formalized correctly, other users can build on it. Without a library, every user would need to rebuild elementary algebra, number theory, and topology from the beginning. With mathlib, one can import existing structures and prove more advanced results on top of them.
For a researcher, mathlib changes the practical meaning of Lean. Lean is not only a blank logical system. It is an ecosystem in which many parts of modern mathematics have already been encoded.
Lean Compared with LaTeX, Python, and Mathematica
It is useful to compare Lean with tools you may already know. LaTeX is for writing mathematics beautifully, but it does not check whether the proof is valid. Python is excellent for computation, simulation, data analysis, and prototyping, but it usually does not prove that the program satisfies a mathematical specification. Mathematica and similar systems can manipulate symbolic expressions, but symbolic manipulation is not the same thing as a fully checked proof.
Lean occupies a different role. It asks us to define objects precisely and prove claims rigorously. This makes Lean slower at the beginning but much stronger when correctness matters. It is not a replacement for Python in numerical simulation, and it is not a replacement for LaTeX in book design. Instead, Lean is closer to a laboratory for formal reasoning.
A good workflow in scientific research may use all three. Python can explore examples numerically. LaTeX can communicate the result beautifully. Lean can formalize the definitions and check the proof of the core theorem.
A Small Example: Programming and Proving Together
Here is a compact example showing Lean’s dual nature:
def square (n : Nat) : Nat :=
n * n
theorem square_zero : square 0 = 0 := by
rfl
The first part defines a program, square. The second part proves a theorem about that program. The theorem says that the square of zero is zero. Lean accepts the proof by computation.
This small example contains the essential pattern of Lean. First, define an object. Then state a property. Then prove the property. The same pattern scales from elementary arithmetic to advanced mathematics, although the proof effort becomes much larger.
Why Lean Matters for Quantum Information Research
For quantum information theory, Lean is interesting because many arguments depend on delicate linear-algebraic assumptions. We often say things such as “let \(U\) be unitary,” “let \(\rho\) be a density operator,” “let \(\{E_i\}\) be a POVM,” or “let \(\Phi\) be a completely positive trace-preserving map.” In informal writing, these assumptions may be clear to the author but easy to misuse in a long derivation.
In Lean, the goal would be to encode these objects with their required properties. A density operator should not merely be a matrix; it should carry positivity and trace-one assumptions. A unitary should carry the property \(U^\dagger U = I\). A POVM should include positivity and completeness. Then, when proving a theorem, Lean forces every step to respect these assumptions.
This does not mean Lean will automatically prove quantum theorems. Formalization can be difficult, especially when the necessary library infrastructure is incomplete. But Lean can help expose hidden assumptions, missing hypotheses, dimension mismatches, and unjustified algebraic steps. For theoretical work, that is extremely valuable.
What Lean Is Good For
Lean is especially good when the cost of being wrong is high. It is useful for formalizing mathematics, checking proof dependencies, verifying algorithms, building certified software components, experimenting with foundations, and creating datasets for AI systems that learn mathematical reasoning.
Lean is less ideal for quick numerical work, ordinary web development, machine-learning pipelines, or exploratory scripting. For those, Python, Julia, JavaScript, Rust, or C++ are usually more convenient. Lean’s advantage is not convenience in the ordinary programming sense. Its advantage is rigorous correctness.
The Main Mental Picture
The best mental picture is this: Lean is a language in which definitions, programs, propositions, and proofs live in one unified typed world. A program has a type. A theorem has a type. A proof is a term of that theorem-type. The kernel checks whether the term really has the claimed type. If it does, the theorem is accepted.
So Lean is not merely a programming language and not merely a proof checker. It is a disciplined environment for building mathematical objects whose meanings are precise enough for a machine to verify.
In ordinary programming, the final question is often whether the program produces the expected output. In Lean, the deeper question is whether the claimed structure, theorem, or program property has been proved from the stated assumptions. That is the central reason Lean matters.
References
Bibliographic Form
Leonardo de Moura and Sebastian Ullrich, “The Lean 4 Theorem Prover and Programming Language,” Automated Deduction – CADE 28, Lecture Notes in Computer Science, vol. 12699, Springer, 2021.
The mathlib Community, “The Lean Mathematical Library,” Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 2020.
Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich, Theorem Proving in Lean 4, online book.
David Thrane Christiansen, Functional Programming in Lean, online book.