Frequently Asked Questions

Is Lean only useful for formalizing mathematics?

Lean’s mathematical library, Mathlib, is impressive, but Lean itself is useful not just for verifying mathematics, but equally suitable for verifying software, hardware, protocols, and more. Lean is also a powerful tool for software development.

Is Lean only a theorem prover?

Contrary to other proof assistants, Lean is a full-blown programming language. Lean is a theorem prover and a general-purpose programming language. Dependently typed pure functional programming has a lot to offer for building reliable, maintainable software, even without formal verification.

Lean’s ahead-of-time compilation to native code together with its runtime with non-tracing garbage collection and mutable in-place updates allows Lean programs to run at speeds that exceed those of interpreted languages, is competitive with other functional programming languages, and can be close to that of C or Rust.

Is Lean just like Rocq?

On a foundational level, Lean and Rocq (the theorem prover formerly known as Coq) have much in common: both are based on dependent type theory (Calculus of Inductive Constructions), with some technical differences:

• Lean has propositional irrelevance.

• Lean uses a non-cumulative hierarchy of universes, while Rocq uses a cumulative hierarchy.

• Rocq’s basic theory supports recursion and its kernel has a trusted termination checker, while Lean’s basic theory only provides recursors and the handling of recursion is not part of the trusted code base.

On top of these similar foundations, however, the systems are engineered rather differently. Lean’s most important design goals are scalability, automation, and a focus on classical logic. Lean is also known for its excellent metaprogramming framework where Lean itself is used for metaprogramming and extensibility. Lean is also written in Lean, and many users have written their own extensions. Lean also provides a rich and modern user interface.

Is Lean’s logic classical?

The foundational logic of Lean is not inherently classical. Just as in Rocq, the Axiom of Choice is an optional axiom that can be used or not.

However, Lean’s standard library, Mathlib, and tactics use this axiom freely, just as a "classical" mathematician would without hesitation. It is not a goal of the Lean project to provide a test bed for constructive mathematics.

Is Lean just like Isabelle?

On a foundational level, Lean and Isabelle/HOL are quite different: Lean is based on dependent type theory and constructs explicit proofs passed to a trusted small kernel, while Isabelle/HOL is based on higher-order logic (HOL) and uses the LCF approach.

Are dependent types natural for formalizing mathematics?

Although at first glance most mathematicians do not learn about “dependent types,” it is a natural, convenient, and powerful framework to express most of mathematics. There is overwhelming consensus in the mathematics community that dependent types are more suited to formal mathematics than HOL.

Typed logics are more ergonomic than untyped set theory, as the type system takes care of many membership proof obligations.

Furthermore, dependent type theory can very naturally express concepts where a mathematical object that is expressed as a type (such as a particular vector space) is parametrized by elements of another type (such as the tangent space for each point of a manifold with borders).

The success of Lean’s mathematical library and its adoption by mathematicians from the level of undergraduate teaching to Fields medalists shows that dependent type theory is not an obstacle for formalizing mathematics.

Are proof objects a bottleneck?

Lean works with proof objects: The user-written proof scripts and tactics are executed to produce an explicit term in the foundational logic that represents that proof, which is then passed to the small trusted component (the kernel) for verification. This way, the soundness of Lean as a theorem prover does not depend on the correctness of the elaboration steps and tactics.

The impact of proof objects in practice is less than often assumed, due to a number of engineering choices in Lean: The Lean kernel supports sharing of subterms in proof objects and lazily evaluates them. Proof terms of user theorems are usually not loaded when importing modules. With Lean’s module system they need not even be distributed with libraries.

The use of proof objects brings important advantages:

• Proof objects can be exported and then checked independently from the main Lean process, by a separate process, or even on separate machines or at a later time. This is more important than ever with the advent of large AI-generated proofs. For example, Nanoda is type/proof checker for Lean implemented in Rust.

• Meta-programs can construct the pieces of a proof directly, without having to go through a soundness-critical builder interface.

• Meta-programs can inspect proof objects. This can be used to implement features like Lean’s "functional induction" or mathlib’s to_additive transfer.

Does dependent type theory hinder SMT integration or other strong automation?

It may seem that a theorem prover based on a simpler type theory than dependent type theory would be better suited for integrating strong automation such as SMT solvers. This is refuted by the grind tactic, which goes beyond attaching external SMT solvers to the theorem prover, and instead implements SMT-like reasoning within Lean’s metaprogramming framework directly, designed for full dependent type theory from the ground up.

Why is 1/0 = 0?

Mathematical division is not defined for zero denominators. There are multiple ways to handle this in a theorem prover: restricting the domain by requiring a proof that the denominator is not zero, returning the result wrapped in an option type, or by extending division to a total function that returns 0 when the denominator is zero. The latter approach is most convenient, avoiding the need to carry around proof obligations or perform case analysis at every step, and is standard in theorem provers. This is still compatible with the standard mathematical theory, as there division by zero does not occur.

For the same reasons, 0 - 1 = 0 holds for natural numbers.