Can we prove every provable statement with Lean?

This question was originally posted on math.stackexchange. People there directed me here. I just discovered Lean and using computers for stating and proving theorems. The first question that came to my mind, can we write any proof with Lean? Or are there limitations (something that you can write a proof for on paper but not in Lean)? I'm not talking about practicality or feasibility. But does the Lean system have the capability?

$\begingroup$ I also feel like there's something about some certain class of recursive functions that can't be proved due to how well-foundedness is implemented $\endgroup$

$\begingroup$ @It'sNotALie. Lean can define all ZFC-provably terminating recursive functions, and the rest I think has the same nature as Gödel's incompleteness. The problem you mention only prevents one way of defining them. $\endgroup$

4 Answers 4

The problem is that your question isn't quite well-formed. To talk about all provable statements, you have to ask what system they're provable in. There's lots of different proof systems!

Lean is an implementation of intuitionistic type theory. By definition, anything provable in intuitionistic type theory is provable in Lean. (It's worth noting that I'm sweeping some things under the rug here: there's lots of different variations on intuitionistic type theory; it's only true that Lean can prove anything provable in its variant.)

You can then ask: how does intuitionistic type theory compare to other proof systems? It's actually a very powerful theory: it's as powerful as second-order intuitionisitic logic with an equality operator. In fact, Lean adds more in the form of inductive propositions.

However, no proof system is all-powerful. For instance, Lean cannot prove $p \lor \lnot p$ . This is a fundamental choice of intuitionistic systems, but of course classical systems (such as classical second-order logic) allow this!(In fact, assuming $\forall P, P \lor \lnot P$ is enough to turn intuitionistic second-order logic into classical second-order logic.)

There are also logics that allow you to ask questions that aren't even well-formed in Lean. For instance, temporal logics allow you to talk about things that are true for some amount of time, but may not be true later. This is really useful when reasoning about invariants in programs, for example.

In sum: Lean is a very powerful logic! But it's not all-powerful, because there is no such thing as an all-powerful logic. In fact, it's less powerful (in some sense) then the logic you're probably most familiar with, due to its intuitionistic nature. However, many of the theorems that you know can be proven constructively, and these proofs are usually considered to be more elegant and beautiful than their classical counterparts.

$\begingroup$ I think the question implicitly assumes any axiom that mainstream Lean users use. (Or maybe what Init or Std uses.) So excluded middle and choice etc are included in the system. $\endgroup$

Yes, in Lean we can write down the proof of any statement that has a proof in the formal system implemented by Lean.

Consider this claim which I think is basically true:

• If a "mathematical statement" is "provable", then it is "provable in Lean".

There are a few pedantic clarifications we need to address:

What do we mean by a "mathematical statement"?

This can be a bit tricky since some statements like "This sentence is false" are not mathematically precise. But even in a formal language, some statements are which are precise are almost meaningless. Take the classic example of $\exp \neq \pi$ ? In ZFC set theory this is well-defined. Everything is a set and all pairs of sets are either equal or not. But its answer is silly and entirely dependent of implementation details of how you defined the real numbers and functions on the real numbers. In Lean, thankfully, this is not well defined because $\exp$ and $\pi$ are elements of different types. Nonetheless, you can still get meaningless statements in Lean such as $\mathbb \neq \mathbb$ which is neither provably true nor false in Lean, because again it depends on implementation details and Lean doesn't bother to clarify how equality of inductive types behave. (Homotopy Type Theory with Univalence on the other hand does prove that $\mathbb = \mathbb$ because they are set types of the same cardinality.)

Another slightly related problem is that some concepts in one logic don't extend one-to-one in another logic. For example, the concept of set has two slightly different translations in Lean. When one talks about a group or topological space being a "set with [various extra operations and properties]", the natural translation is to say "type" instead of set. But when on talks about the union of two sets, then one is taking about subsets of a type (which Lean just calls sets). But again, this is mostly implementation details and there is no ambiguity in practice.

What do we mean by "provable in Lean"?

Lean is a formal system, so in one sense it is clear what it means to be provable in Lean. But there are a few subtleties: First, the base logic of lean is constructive mathematics, so you can't prove say the intermediate value theorem in base Lean. But in practice, Lean uses classical logic including the axiom of choice. (Indeed, it is really hard to use Lean without the axiom of choice since the usual tactics sort of sneak it into your proofs.) So let's assume we mean Lean with all its axioms.

Second, Lean is implemented on a physical computer. It wouldn't be too hard to come up with (short) theorem statements which would make Lean's type checker crash even on a super computer. And similarly, there are pathological theorems which are easy to state, but whose proof would take more than the size of the universe worth of code to prove. However, I don't think this is an issue in practice.

What do we mean by "provable"?

I assume you mean, roughly, provable in the mathematical literature. Since some "proofs" are wrong, I also assume you mean proofs that are correct.

It's been argued by various people that when we say something is mathematically proven, that this is equivalent to saying it could in principle be formalized in a standard formal system. As others here have said, if that formal system is Lean, we are done, but let's take it to be ZFC or ZFC plus universes (which some argue are important for a lot of the mathematical reasoning used today). That makes the question interesting and better ties into mathematical history.

Now, whether informal mathematics is really translatable to formal mathematics is a philosophical question, but on a practical level it seems to be true. I am not aware of a theorem of mathematics that we know can't be formalized in at least some standard formal system, and we have already formalized a large amount of mathematics both in practice and in theory. And ZFC plus infinitely many universes seems to be a good enough foundation in practice (or so it seems to me).

Roughly, everything that is provable in ZFC plus infinitely many universes is provable in Lean (with the axiom of choice), and vice versa. The precise details (to again avoid talking about silly mathematical statements) is stated more precisely in Mario's Carneiro's thesis, but in particular it does cover all arithmetic statements.