Tutorials for mathematicians with programming background?

Stream: new members

[William]

Are there any tutorials out there that assume the reader already knows how to write proofs and understands basic logic, doesn't care about the details of Lean's implementation, and just wants to know the bare minimum syntax to formalize, check, or generate proofs?

E.g. which keywords, which punctuation, in which order, etc.

For example, trying to look at examples from tutorials, I thought that it should be straightforward to check that 2+2=4 and that 2+2 does not equal 5. But the output #0 from Lean does not seem to mean anything (it returns the same for both the true statement and the false statement, and doesn't say anything unambiguous like "this evaluates to true" or "this evaluates to false").

#check 2+2=4
#eval 2+2=4  -- neither returns something clear like "True" as output

#check 2+2=5
#eval 2+2=5 -- neither returns something clear like "False" as output

Is it a typing issue and I have to specifically declare 2, 4, and 5 as natural numbers before I can check the validity of these statements? If so, fine, but then what is a minimum working example that shows or validates or checks that 2+2=4 is true for natural numbers, and 2+2=5 is false for natural numbers?

Do users really need to know all about dependent type theory and tactics and a million other things to understand the code syntax of the very fist, simplest examples of verifying that 2+2=4 and that 2+2 does not equal 5?

Like sure syntax can sometimes have different or more general meanings in different contexts, but I'd like to be able to learn by copying-pasting-modifying simple examples I understand either until they break or they do things that are more complicated and interesting to me.

Maybe as a more non-trivial example of what kinds of tutorials I'm looking for, I'm not able to check the validity of basic predicate logic statements, and the tutorials I've been able to find have a lot of information extraneous to my goal: get an unambiguous report of "True" or "False".

As one example: https://leanprover.github.io/logic_and_proof/first_order_logic_in_lean.html <- Is the letter h somehow a keyword in Lean? It seems to be used like one in those examples, but if so its syntactical role is never explained or mentioned. The tutorial is partially helpful, but not enough to get me all the way to my end goal.

Here is a simple example of the kind of basic statements I'd like to write in predicate logic, and whose validity that I would like to check.

open classical

constant x: Type -- undefined, primitive sort
constant P: x → Prop -- undefined, primitive predicate

axiom test: ∃ y: x, P(y)

example (y:x):  ¬ (∀ y, ( ¬ P(y) )) :=
assume test,
sorry  -- how do I show that this is true given test?

#eval ¬ ∀ y:x, ¬ P(y)
#check ¬ ∀ y:x, ¬ P(y)

example (y:x): ∀ y, ¬ P(y):=
assume test,
sorry  -- how do I show that this is false given test?

#eval ∀ y:x, ¬ P(y) -- neither of these
#check ∀ y:x, ¬ P(y) -- seem to work

I get that in constructive logic, without excluded middle, we don't necessarily have that the universal and existential quantifiers can be defined in terms of each other. And I get that Lean supports constructive logic by default, with classical logic as a special case. But beginning the code with open classical doesn't seem to be enough. Instead running Lean on the code gives me an error about has_repr type, and says nothing about whether the statements are True or False. This is confusing to me both as someone trained as a mathematician using classical logic, and as a programmer who uses languages that have Boolean types with unambiguous True or False values.

(Also even in constructive logic the second example should still be False I think, even if the first example need not be True nor False.)

Anyway all I'm asking for is for dumbed-down, basic tutorials that explain the programming language syntax for showing that certain statements are True and False, and how to read/understand the output from Lean for whether it is telling you that something is True or False.

[Damiano Testa]

Does #eval (2+2 = 4 : bool) give something better?

[Damiano Testa]

Does #eval (2+2 = 4 : bool) give something better?

[Damiano Testa]

(I'm on mobile, hence the duplicate message :oh_no:)

[Damiano Testa]

Anyway, the short summary is that writing #eval 2+2=4 basically gets lean to the stage where it realizes that it has a proposition, namely the assertion that 2+2 equals 4, but does not find a truth value for it, since in general, there is no decision procedure for a proposition. With the explicit type ascription (to booleans, rather than Propositions), you tell Lean to try harder and then it realizes that there is a decidable instance somewhere that allows is to actually compute the truth value of this specific proposition, and then it should report tt: the proposition is true.

[Kyle Miller]

@Damiano Testa That's how Lean 4 #eval works, but in Lean 3 you get #0 for a proposition since this command is a front-end for the VM compiler and evaluator, propositions are computationally irrelevant thus erased, and as an implementation quirk the result of computing nothing is this #0 thing.

[Kyle Miller]

In Lean 4, there's a check that turns #eval p into #eval decide p if p is a proposition.

[Kyle Miller]

@William Lean is meant to be a system where you interactively construct proofs of propositions rather than one that automatically decides whether a proposition is true or false. The #check command is simply meant to give you the type of an expression (after checking it is well-typed) and #eval is meant to evaluate Lean-as-a-programming-language, and it strips out all propositions since these are considered to have no computational content.

[Mario Carneiro]

constant x: Type -- undefined, primitive sort
constant P: x → Prop -- undefined, primitive predicate

axiom test: ∃ y: x, P(y)

theorem test' :  ¬ (∀ y, ( ¬ P(y) )) :=
assume not_test,
let ⟨y, hy⟩ := test in
not_test y hy

#eval (¬ ∀ y:x, ¬ P(y) : bool) -- fails because there is no decidability instance for this proposition
#check ¬ ∀ y:x, ¬ P(y) -- it's a prop
#check (test' : ¬ ∀ y:x, ¬ P(y)) -- it's a true prop, because test' is a proof of it

example : ∀ y, ¬ P(y) :=
assume test,
sorry  -- we can't prove it, so there isn't much hope here


#check ∀ y:x, ¬ P(y) -- it's a prop
#eval (∀ y:x, ¬ P(y) : bool) -- but we still can't evaluate it like this

-- Since we proved it is false, we can inform lean of it using this instance
instance : decidable (∀ y:x, ¬ P(y)) := is_false test'

-- and now these work:
#eval (¬ ∀ y:x, ¬ P(y) : bool) -- tt
#eval (∀ y:x, ¬ P(y) : bool) -- ff

[Niels Voss]

Note that unlike in logic the keyword assume has nothing to do with the keyword axiom, so saying something like assume test is probably not what you want to do. If you want to prove P → Q (which of course means "if P then Q") then writing assume h creates a new variable called h which records the fact that P is true, and then switches to you trying to prove Q. assume actually has very little to do with assuming things.

One very important thing about Lean is that it uses the propositions-as-types paradigm. What this means is that if P is a proposition, then P can also be seen as the type of proofs of P (this is a confusing statement and it takes time to get used to). So P → Q can also be seen as the type of functions which take proofs of P as input and output proofs of Q. In this sense, the keyword assume is almost exactly the same as python's keyword lambda.

Also, you're probably aware of this, but the primary role of Lean is to verify that your proofs are correct, rather than to prove complex statements on its own. So there's no command to check whether or not a given statement is true. If you do want to have Lean attempt to generate a proof of a statement, you can use something called tactics (in particular, writing by tauto will have Lean try to generate proofs of first order logic statements), but note that these usually can't prove anything super complex.

[Heather Macbeth]

William said:

Are there any tutorials out there that assume the reader already knows how to write proofs and understands basic logic, doesn't care about the details of Lean's implementation, and just wants to know the bare minimum syntax to formalize, check, or generate proofs?

E.g. which keywords, which punctuation, in which order, etc.

@William The canonical answer for someone asking for a "tutorial for mathematicians" is Mathematics in Lean. Have you already looked at this?

Do users really need to know all about dependent type theory and tactics and a million other things to understand the code syntax of the very fist, simplest examples of verifying that 2+2=4 and that 2+2 does not equal 5?

It's true that in Mathematics in Lean, the proof that 2 + 2 = 4 will go via a tactic (possibly rfl or decide, but these are still tactics) rather than in term mode. That's because mathematician users of Lean tend to rely heavily on tactics rather than writing term proofs for everything, so the book gets started early with explaining tactics. Perhaps your use case is different, feel free to explain.

On the other hand, for the impatient, I have found that simply mousing through the infoview in a proof of a theorem you know well can be a good way to get started. It should be a fairly advanced/abstract theorem, otherwise you will have the problem that the mathlib implementation has been transformed or splintered beyond recognition from the version you know. If you want to tell us your field, people can probably suggest an interesting file to look at first.

Definitely you don't need to know anything about dependent type theory for your first month.

[William]

Sorry for the slow response everyone, I thought people would be too busy to read / see this anytime soon and so wasn't expecting responses so soon. Everyone's enthusiasm and helpfulness is amazing! I really appreciate it.

@Heather Macbeth Thank you so much for this! https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html#getting-started

I actually didn't know that this existed at all, the first page even has the 2+2=4 example, haha.

This is perfect. I will definitely have to spend a lot of time working through that from now on.

@Niels Voss The explanation of assume is very helpful, I was definitely completely misunderstanding it. Also the explanation of where these h variables in the tutorials come from also really helped.

@Mario Carneiro Thank you so much for the line-by-line explanation of that example! I was getting really frustrated because the behavior wasn't what I naively expected at all, but this is much clearer now. I still have to think through it more though, but I really appreciate the time you spent to help me.

@Kyle Miller I was also really misunderstanding the points you mentioned too. In particular the difference in purposes between tactics and type checking in Lean. The explanation of Lean vs Lean 4 is also really helpful -- it looks like there'll be a lot to look forward to in the new release!

@Damiano Testa Thank you for the explanation of this! I didn't understand the purpose of the eval keyword at all, nor when to use propositions vs when to use booleans (or even whether Lean had booleans). This is all much more clear to me now.

@ everyone
I'll have to spend a lot more time getting used to Lean and working through examples to become productive with it at all, but you've all given me the confidence that this is not a hopeless task and that it really is worth trying after all! I had been getting really frustrated failing with such simple examples, so all of these explanations really mean a lot to me, and again I really appreciate all of the help from everyone! Thank you all so much again!