3
$\begingroup$

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?

$\endgroup$
3
  • 3
    $\begingroup$ Gödel's second incompleteness theorem applies here. $\endgroup$
    – Trebor
    Aug 15, 2023 at 13:08
  • $\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$ Aug 15, 2023 at 13:11
  • $\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$
    – Trebor
    Aug 15, 2023 at 13:19

4 Answers 4

8
$\begingroup$

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.

$\endgroup$
1
  • 7
    $\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$
    – Trebor
    Aug 15, 2023 at 15:43
3
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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{N} \neq \mathbb{Z}$ 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{N} = \mathbb{Z}$ 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.

However, if one wants to be pedantic about what is and isn't provable, one has to be a bit careful. One way to get around this is just to talk about the theorems in "arithmetic", namely the natural numbers with $+$, $*$, $<$, $0$, and $1$ and high order logic quantifiers over the natural numbers. Then there is no ambiguity. Every major set-theory-like formal system can express arithmetic statements. And conversely, a huge chunk of mathematics can be translated to statements in arithmetic.

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.

$\endgroup$
0
$\begingroup$

For standard statements and proofs in mathematics, I would say that it is possible to implement them in principle. Evidence of this is that parts of very diverse areas have already been formalized, see this list or this one about undergraduate mathematics.

However, it is not possible to implement everything in one version of Lean, due to Gödels incompleteness theorem. Lean can be viewed as a formal system capable to define the natural numbers. Hence there are some mathematical statements that can be stated in Lean, but for which there is no proof within Lean.

An example would be statements about Lean itself: Consider the set of real numbers that can be defined in Lean and call it $C$. We can argue that this set is countable, since we can lexicographically order the Lean-code for these numbers. If it were possible to define the set $C$ in Lean and write a Lean-proof that $C$ is countable, then one could write a Cantor-diagonal-trick-type-proof to show within Lean that $C$ is uncountable. Therefore the set $C$ and statements about its cardinality are something that cannot be done in a proof assistant.

$\endgroup$
5
  • 4
    $\begingroup$ I don't think that Godel actually plays a role in this question. It was about provable things, not true things. So while your answer is accurate---there are true things (in any particular model of Lean) which are not provable---it's not about what the questioner is asking. $\endgroup$ Aug 15, 2023 at 15:00
  • $\begingroup$ @AndrewK.Hirsch , Thank you for your comment. The example of the statement "C is countable" seems to be a "concrete" example of something that is provable on paper, but not provable within Lean. Are you saying this example does not answer the question, or are you saying that this example is not about Godel incompleteness? $\endgroup$ Aug 23, 2023 at 11:54
  • $\begingroup$ I don't think it's really an answer to the question, and I'm not even sure it's correct. Note that what looks like the same question (does C have a countable cardinality) is actually two different questions: one is "does the set C of formal lean-objects representing real numbers countable" and the other is "is the set of real numbers (internally) countable". These are different questions, with opposite answers! $\endgroup$ Aug 23, 2023 at 14:14
  • $\begingroup$ I don't see how the second question "is the set of real numbers (from the point of view of Lean) countable?" comes up. The set of real numbers as defined in Lean is very different from $C$. $\endgroup$ Aug 25, 2023 at 8:03
  • $\begingroup$ I misread the example. Reading it now, it's just not true: I can absolutely build a model of lean in lean and then show that the set C is countable. There's no diagonalization trick to be played. (If you knew that C was a model of the real numbers, and you had a classical definition of the real numbers, you might have a problem). All Goedel prevents me from doing is proving the soundness of lean in lean, not modeling things like this. $\endgroup$ Aug 25, 2023 at 21:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.