Lean basics documentation

Stream: new members

[Fredrik]

I'm currently making a second attempt to learn Lean. I've found it very challenging so far, as all resources jump into explaining various things within a certain context without explaining the context, as if assuming that the reader is already familiar with Lean. I've searched through the Lean Manual and Theorem Proving in Lean 4 and couldn't find any explanation of the keywords example, lemma and theorem. Is there some documentation available somewhere?

[Fredrik]

The Tour of Lean in the Lean Manual is a striking example. Even before the chapter explaining how to install Lean, it assumes that the reader already knows Lean well enough to be able to read a several pages long module showcasing a variety of language features that are not explained in the manual.

[Ruben Van de Velde]

theorem is introduced here in tpil4: https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html

lemma is just a synonym for theorem

example is introduced here: https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html?highlight=example#conjunction

[Ruben Van de Velde]

I'm guessing the intention of the manual is more "this is what lean looks like" than expecting a newcomer to understand it all

[Fredrik]

Ruben Van de Velde Thank you. It wasn't obvious that these are the places these concepts are introduced.

[Adomas Baliuka]

On this note, is theorem also the same as def? The effect seems to be very similar.

[Ruben Van de Velde]

From my first link:

Note that the theorem command is really a version of the def command: under the propositions and types correspondence, proving the theorem p → q → p is really the same as defining an element of the associated type. To the kernel type checker, there is no difference between the two.

[Scott Morrison]

@Fredrik, perhaps if you describe your background a little (programming, CS, mathematics research?) we can point you to better starting places.

[Fredrik]

Scott Morrison Good point. My background is in systems development, programming languages and compilers, mainly languages of practical use for systems development (C, Rust, Python, etc.) as opposed to languages that are there just to be theoretically interesting for mathematicians (Haskell), and I want to use Lean for proving the correctness of programs. Anything that uses mathematical notation or vocabulary tends to confuse me, but when it gets translated to a domain that I understand, I tend to see how simple it is.

One thing that made me start to understand Lean is the insight that a proposition is the same thing as a set, and a set is the same thing as a type in a programming language, and a proof is the same thing as a member of a set, and a member of a set is the same thing as a value of a type, and constructing a proof of a proposition is the same thing as producing a value of a type by using definitions that have already been made, either directly or calling them as a function that produces a value of one type from a value of another type.

[Ioannis Konstantoulas]

I think the proper starting point is the book Functional Programming in Lean. It is by far the most accessible resource.

[Kevin Buzzard]

Accessible is very much in the eye of the beholder! I would say that mathematics in Lean is far more accessible, but then I am a professional mathematician with very little programming experience.

[Fredrik]

Ioannis Konstantoulas That book was not yet written when I made my first attempt to learn Lean, so it's very helpful that you pointed it out. This sentence (as well as the rest of the paragraph) in the introduction appeals to me:

This book is intended for programmers who want to learn Lean, but who have not necessarily used a functional programming language before.

[Fredrik]

Kevin Buzzard You're the one who made the natural numbers game. :big_smile: Thank you. I studied the whole thing and I liked it a lot. It was however very confusing at first to write the code that goes inside the proofs without understanding the basic structure of Lean that surrounds the proofs. I would have got started much quicker if I had first understood the basic structure of a Lean file.

[Ruben Van de Velde]

I had the opposite experience, personally - I found it much easier to get started with the NNG focusing on just the proofs

[Fredrik]

Ruben Van de Velde I suppose it depends on your background. If you're familiar with doing proofs by hand, the NNG focuses on the relevant parts of Lean, whereas as someone who understands programming languages well, but can't do a proof by hand, I can figure things out by first knowing the language and what the computer will do with it.

[Kevin Buzzard]

@Fredrik I would recommend #tpil if you want to see the details of the terms. It's been empirically observed for years on this site that there are many users (typically with computer science backgrounds) who really want to understand the concept of what a Lean type and term are and how to write code, and will move on to tactic from there; conversely there are also many users (typically with mathematics backgrounds) who want to see how an ITP does mathematics -- how it thinks about mathematics -- and how to use tactics, before ever caring about the underlying type theory (mathematicians typically are taught mathematics with no explanation of the foundations). One big difference is when tactics are introduced; TPIL doesn't introduce them until chapter 5 whereas NNG introduces them immediately, for example. One question which might distinguish the CS people from the maths people -- do you care about the actual term produced by a tactic, or do you just want to apply the technique which it has packaged up and then move on to the next line of the proof?

[Kevin Buzzard]

ooh the linkifier is still linking to the Lean 3 version so it seems: I mean this https://leanprover.github.io/theorem_proving_in_lean4/ .

[Niels Voss]

ab said:

On this note, is theorem also the same as def? The effect seems to be very similar.

If I remember correctly, theorem is the same asnoncomputable def

[Mario Carneiro]

no, they are different

[Mario Carneiro]

I believe noncomputable is an independent setting

[Mario Carneiro]

theorem is closest to @[irreducible] def, but it has different elaboration behavior (the type is required and the body cannot influence the type)

[Mario Carneiro]

Actually you are right, theorem implies noncomputable