how to learn lean?

Stream: new members

[Hbz]

I want to prove some proofs on the lean, but i find that i can't use some tactics or something smoothly, So, how do you make the transition from the beginner stage, and how to learn to use some basic methods?need some suggestions! :blush:

[Kenny Lau]

try to do something basic, or something that is already in mathlib, and then compare the proofs

[Kenny Lau]

btw lean is more than just the proofs, eventually you will need to learn how to make good defs

[Kenny Lau]

(which include structure and class and inductive)

[Hbz]

Thank you!
:joy:

[Michael Rothgang]

Just In case you haven't seen it yet: mathematics in Lean #mil is a good learning resource.
It's more advanced than the natural numbers game, but does not assume a lot of knowledge. (Some of the later chapters assume some mathematics knowledge. If you don't know that and don't want to formalise anything using these concepts, you can certainly skip them at first.)

[Michael Rothgang]

Moving beyond MIL, in my experience the best way to learn is do a small "project": choose something you want to formalise and try it. You will (probably) get stuck at times, that's normal (and past of learning process). Don't hesitate to ask for help on zulip!

[Michael Rothgang]

And, of course: learning or working together can be a lot of fun. If there are fellow Lean enthusiasts near you, talk to them :-) There is a community map https://leanprover-community.github.io/meet.html, or you can see if the Geographic locality stream has a channel close to where you are.

[Hbz]

Thank you very much for your suggestions. (As a Chinese person, my English expression may not be very accurate, so please forgive me.) Although Lean sometimes makes me frustrated, after solving some problems that have troubled me for a long time, I also feel a strong sense of accomplishment. This is probably my motivation for learning Lean. There is an ancient Chinese saying: "When one is surrounded by mountains and rivers with no apparent way out, suddenly a village appears with willows and flowers in full bloom." I plan to use the #mil you mentioned to consolidate my foundation. Thank you again for your suggestions! :slight_smile:

[suhr]

I can a few advises:

• Lean how things work under the hood. Learn not only tactics, but also terms, know which terms tactics generate, lean typing and computation rules
• Build vocabulary. Natural number game not only teaches you how to use Lean, it also gives you a set of tools (lemmas) to work with natural numbers effectively. But for other things you will need to build a vocabulary yourself
• The reason why something is hard to proof is often the lack of lemmas

[Michael Rothgang]

Heather Macbeth is often quoted as saying that you shouldn't need to remember lemma names --- if you do, there's a missing tactic. At the moment, that's only an aspirational goal for mathlib (you can do that often, but not always!). Still, I'd like to emphasize this point: learning about the various tactics can be really helpful.

[Michael Rothgang]

This page https://leanprover-community.github.io/mathlib-manual/html-multi/Tactics/All-tactics/#all_tactics has a list lists pretty much all tactics in mathlib, grouped also by what they do/the area you can use them in.

[Kenny Lau]

also, learn to use loogle and leanexplore and leansearch

[suhr]

rw? and apply? are also very useful (but I wish there were smarter versions of them).

[JK]

I have to say that I have also found it extremely frustrating to use Lean. I've tried both the Mechanics of Proof and the Mathematics in Lean tutorials, and I find that they don't do a very good job of explaining the mechanics of using tactics. My approach so far has been to ask (stupid) questions here, and otherwise try to pattern-match from other examples I can find. Are there other tutorials out there that focus less on the math and more on the way to structure proofs in Lean and how to approach using tactics?

[Kenny Lau]

I'm not sure what you mean. The number 1 advice has always been, write your proof on paper first, and make sure you justify every single step, and then translate each step into Lean

[Kenny Lau]

I guess it would also be helpful if we have a short tactic guide

[Matt Diamond]

when you say "the mechanics of using tactics" do you mean knowing which tactics to use or understanding the syntax of how to use them, or perhaps both?

[JK]

I'm stuck on Example 2.1.8 in Mechanics of Proof now. The proof on paper is written out. But (1) I can't see how to prove it without introducing several hypotheses using "have" followed by a "calc," which I don't think is the intention and seems like bad style for such a simple proof; anyway, (2) I'm stuck with the following (simplified)

example (a b : ℝ) : 3 * (b+a)^2 ≥ 0 := by
  have sq : (b+a)^2 ≥ 0 := by exact sq_nonneg (b+a)
  have h3 : 3 ≥ 0 := by norm_num
  exact Left.mul_nonneg sq h3

I feel like introducing hypothesis h3 should be unnecessary, but in any case I don't see why the final exact is not sufficient to complete the proof. Now, you could tell me the answer (and I'd appreciate it), but then the next time I face a similar situation I feel like I still won't have any idea how to move forward without asking again.

[Matt Diamond]

if people's answers aren't giving you the resources to face similar situations, perhaps they're not answering you well

[Matt Diamond]

one tip: you should rarely need to write by exact... if you find yourself writing that, just remove it

for example, instead of

have sq : (b+a)^2 ≥ 0 := by exact sq_nonneg (b+a)

just write

have sq : (b+a)^2 ≥ 0 := sq_nonneg (b+a)

[Matt Diamond]

by takes you from term into tactic mode, and exact takes you right back into term mode

[JK]

@Matt Diamond I mean even something as simple as explaining "here's how you apply rw to a goal, and here's how you apply rw to a hypothesis."

[JK]

@Matt Diamond and none of the resources (at least from what I have read so far) explained that there are tactic and term modes, or what the difference is!

[Matt Diamond]

ah, that's frustrating... have you tried reading #tpil? that might help if you haven't yet

[Matt Diamond]

(that's a link to Theorem Proving In Lean)

[Matt Diamond]

just curious, do you know any other programming languages?

[JK]

@Matt Diamond I have not tried #tpil, but I was scared off by the warning that it was more advanced than the others.

I do know imperative programming languages (primarily C)

[Matt Diamond]

oh okay, cool... imho you can think of term mode as essentially "normal programming", where you're assigning variables, passing them into functions, etc.

[Matt Diamond]

tactic mode is the special case... that's what follows by and involves those line by line commands

[Matt Diamond]

I would say give #tpil a shot, perhaps

[JK]

thx

[George Menhorn]

@JK I've been finding that doing these sorts of examples without using tactics at all can help make things clearer in some cases:

example (a b : ℝ) : 3 * (b+a)^2 ≥ 0 :=
   mul_nonneg zero_le_three (sq_nonneg (b + a))

[suhr]

JK said:

I have not tried #tpil, but I was scared off by the warning that it was more advanced than the others.

It's one of very few Lean tutorials which bother to explain how things actually work.

[Matt Diamond]

I'm curious where that warning was and if it should be removed / reworded (unless JK just meant some word-of-mouth thing)

[Hbz]

suhr said:

rw? and apply? are also very useful (but I wish there were smarter versions of them).

I love 'apply?'! :smile:

[JK]

@Matt Diamond OK, maybe "more advanced" is not technically the right term. But quoting from #mil:
"This book is complementary to a companion tutorial, Theorem Proving in Lean, which provides a more thorough introduction to the underlying logical framework and core syntax of Lean. Theorem Proving in Lean is for people who prefer to read a user manual cover to cover before using a new dishwasher. If you are the kind of person who prefers to hit the start button and figure out how to activate the potscrubber feature later, it makes more sense to start here and refer back to Theorem Proving in Lean as necessary."

[Ruben Van de Velde]

JK said:

Matt Diamond I mean even something as simple as explaining "here's how you apply rw to a goal, and here's how you apply rw to a hypothesis."

Hmm, I'm a bit confused. MoP introduces rw in §1.2.1 and immediately shows an example of how to apply it to the goal. It's true that rewriting a hypothesis only seems to come up in §4.5.5, but I'd guess that everything before that should be solvable without doing that. (MoP has somewhat of an idiosyncratic style of proof, so people may come up with other proofs of the exercises that use features not introduced in MoP yet).

That said, people don't all learn in the same ways, so it makes sense that some texts work better than others depending on the person

[Alex Nguyen]

suhr said:

I can a few advises:

• Lean how things work under the hood. Learn not only tactics, but also terms, know which terms tactics generate, lean typing and computation rules

Hi @suhr, is there some resource you'd suggest for learning which terms tactics generate, is it in the #mil resource ?

[suhr]

#print and show_term allow you to look into definitions and terms generated by tactics.

Alex Nguyen said:

is it in the #mil resource ?

No, #mil does not explain anything at all. #tpil is much better in this regard, it shows how to work with basic things without tactics (for example, it shows you Eq.subst, so you could figure out how to do rewriting without rw). It does not give you too much details though.

The only tutorial I'm aware of which makes a more serious attempt to explain how things work is my own book. For example, when discussing equality, it introduces both Eq.subst and Eq.ndrec (https://suhr.github.io/tmath/basics/lean.html#id4). Moreover, it shows how to use them (with explicit motives) to prove basic properties of equality.

This is already way more than you can find in #tpil, but then it shows how you could prove inequality from the first principles.

The book does not dive into how tactics work though, since it uses only a few of them and the reader already knows how to live without them. But it explains how decide and well-founded recursion work.

[Kaixin Wang]

Redacted

[Alex Nguyen]

@suhr Thank you !

[Dan Velleman]

@JK Another resource you could look at is How To Prove It with Lean.

[Paolo Scarpat]

JK said:

I have to say that I have also found it extremely frustrating to use Lean. I've tried both the Mechanics of Proof and the Mathematics in Lean tutorials, and I find that they don't do a very good job of explaining the mechanics of using tactics. My approach so far has been to ask (stupid) questions here, and otherwise try to pattern-match from other examples I can find. Are there other tutorials out there that focus less on the math and more on the way to structure proofs in Lean and how to approach using tactics?

@JK I often feel the same way. I think Buzzard's Formalising Mathematics does a better job of explaining tactics.

[JK]

@Paolo Scarpat Thank you! This tactic guide was exactly the sort of thing I was looking for.