Learning Lean frustration

Stream: new members

[Victor Miller]

I almost hesitate to post this here. I've been trying to learn learn on and off for the past 4 years. I've plowed through the Natural Number Game, but when it comes to doing something after that I've had nothing but frustration. I'm a mathematician with a lot of programming experience: in the 60 years (really!) that I've been programming I've written substantial programs in at least 50 different languages (including Haskell). Trying to get over the most elementary hurdles in Lean has, by far, been the most frustrating. One thing that has stymied me, is to even know all of the many picky syntax rules. I'm using lean4-mode in emacs (with lsp), and it will flag certain things in red, but never explains what it doesn't like. The tactics are complicated, and ill-defined: they obviously are pattern matches of some sort (including type information). Some apparently take the entire current state as potential input, and some don't: which are they? I've tried to read "Theorem proving in Lean" which is extremely chatty, but in no place does it really nail down what things are.

I periodically set aside a few hours to go back to Lean. In every case, after flailing around for 2 hours I give up. I hope that there are some constructive suggestions for me.

[Henrik Böving]

I'm using lean4-mode in emacs (with lsp), and it will flag certain things in red, but never explains what it doesn't like.

I would suggest to use the VSCode or neovim plugin unless you know what you are doing. The Emacs mode has long been unmaintained and lacks far behind the UX and features that the two maintained editor integrations have.

The tactics are complicated, and ill-defined: they obviously are pattern matches of some sort (including type information). Some apparently take the entire current state as potential input, and some don't: which are they?

If you want to have information about the individual tactis just hovering over them in either of the two well supported editors will give you their documentation, other than that you can also read the language reference manual on the manner, for tactics in particular this chapter

[Michael Rothgang]

In general, if you have a specific example, you can definitely ask for help here. This place is pretty friendly to new contributors, and you usually get help rather quickly.

[Michael Rothgang]

It's a bit hard for me to answer specific questions you have (because I don't know what these are), but if you ask about particular examples, I'm sure people will be happy to help. Lean has a steep learning curve, so asking for help is a natural and healthy thing!

[Mirek Olšák]

I have to admit that tactics are hard to search for. There are good ways to search for theorems: loogle, leansearch, exact?, rw?? (VS Code only), simp?`), but with tactics, the best option is probably still asking here.

[Mirek Olšák]

There is at least a website concatenating the docs of all tactics in a similar way as #help tactic: https://seasawher.github.io/mathlib4-help/tactics/. The reference manual contains some preselected list (I think).

[Michael Rothgang]

Mirek Olšák said:

I have to admit that tactics are hard to search for. There are good ways to search for theorems: loogle, leansearch, exact?, rw?? (VS Code only), simp?`), but with tactics, the best option is probably still asking here.

I dearly hope this is untrue - and if it's still true, this needs to change. With my "instructor for a Lean course" (in Bonn) hat on, I'm also willing to spend some time to change this is needed. That said, I know if at least two resources that are helpful here:

[Michael Rothgang]

https://leanprover-community.github.io/mathlib-manual/html-multi/Tactics/All-tactics/#all_tactics is a list of all tactics in mathlib. It's automatically generated; I'm not sure how often it is updated automatically. (@Anne Baanen Can you clarify this, or help me find out myself? Thanks!)

[Michael Rothgang]

In the side-bar on the left, there are also various categories - so if you're looking for e.g. "analysis tactics", you can click on that category.

[Michael Rothgang]

The second resource is https://leanprover-community.github.io/papers/lean-tactics.pdf, a tactic cheat sheet. It's compact (three pages), and a bit more selective. It doesn't explain each tactic in detail (for that, use the first link - or complain here if anything is unclear; Anne actually has time to work on this!), but should give a good overview.

[Mirek Olšák]

Thanks for these, as someone who plan to teach Lean too, I was quite hesitant which subset of tactics to show (when I want to focus also on many other aspects than tactics), this cheatsheet looks reasonable, just perhaps missing rw! (out of those I was often in touch with).

[Mirek Olšák]

Michael Rothgang said:

In the side-bar on the left, there are also various categories - so if you're looking for e.g. "analysis tactics", you can click on that category.

The "categorized" list of tactics is a bit outdated. Not sure if I would recommend reading that. Missing grind in automation, missing rw?? in interactive...

[Victor Miller]

@Henrik Böving Thank you for the link to the tactic description. However, one thing that I notice is that they don't say (except what you can implicitly infer from examples) whether or not they take arguments. I'm guessing that if they don't, their implicit arguments are the entire current state. As far as vscode, I'll, reluctantly, give it another try. I've tried to use vscode (both with Lean and other languages) over the past 5 years, and I've never liked it. I always feel like I'm looking at my program from the "wrong end of a telescope", and the many popups just seem to interrupt me and get in the way. Maybe there's a way to customize it.

[Niels Voss]

If part of your complaint is that things are not "pinned down" as much as they are in traditional programming languages, you might want to consider learning lean first as a programming language (e.g. by skimming #fpil) and then later learning how to do theorem proving with it. I suggest this only because based on what you said, I'd imagine you're pretty good at picking up new programming languages. This maybe isn't the best idea if your main and only goal is to use Lean for theorem proving. Also note that learning lean as a programming language won't make you better at using tactics.

[suhr]

One thing that has stymied me, is to even know all of the many picky syntax rules.

You don't need to use custom syntax.

The tactics are complicated, and ill-defined: they obviously are pattern matches of some sort (including type information).

And you can avoid using tactics as well.

The core of Lean is not that complex, and everything else is extra on top of it. So you can learn Lean starting from the core, and you can always strip away confusing high level parts when you need to.

[Victor Miller]

@Niels Voss Thanks for the suggestion. From a first glance I see a lot of similarities to Haskell, with which I’m familiar. But your comment about tactics is right. What I wish there was, is a tutorial of a lot of basic tactics: have a lot of examples with the state before and after specified, and allowing the end user to internalize which tactic should apply. My guess is that in tactic structured proofs, the prover (i.e. the human) has in mind what the next state should be and then attempts to use a series of one or more tactics to get there.

[suhr]

NNG does not teach you the core stuff at all unfortunately.

[Weiyi Wang]

A term mode NNG would be interesting

[Riccardo Brasca]

What would you like to do with Lean? Proving theorems? Writing (certified) programs? Even if technically those are the same thing, in practice the way a mathematician or a programmer use Lean is quite different.

[Michael Rothgang]

Have you seen Mathematics in Lean already? Clicking on the link #mil here will take you to it. Its aim is to explain basic tactics and the design of things step by step.

[Michael Rothgang]

Another option: there are a number of university courses using Lean these days, and many of them have public lecture notes. One of them is taught by @Floris van Doorn and myself, look here: https://github.com/fpvandoorn/LeanCourse25. Each file should be self-contained (and runs on mathlib as of mid-October; we did not upgrade this during the semester).

[Michael Rothgang]

The lecture notes certainly have lots of examples, teaching you how to do basic mathematics X in Lean.

[Michael Rothgang]

If you're looking for something more low-level (i.e., with less math background), I would recommend Heather Macbeth' Mechanics of Proofs. It sounds like you know more math than that book's target group, though.

[Dominic Steinitz]

Haskell programmer of 30 years here and also emacs user. Sadly the emacs setup for Lean isn't up to snuff. I have VS Code and emacs open on the same lean file and mainly work in VS Code as for me it's easier to see what is going on. I do move to emacs for e.g. bulk replace / occur - as long as you remember to save then the changes seem to be replicated without having to reload the buffer. The one thing I do find ok in VS Code is the equivalent of M-. and M-, which are fn-F12 and C-- (maybe that is just on macOS).

I am pretty sure (in fact I think I tried this as the beginning of my Lean journey) that as in Haskell you can write a Lean program that is the proof but as far as I can tell no-one does and everyone uses tactics maybe so that the proof then looks like regular math rather than a program. Up to now I have only really used unfold, simp, rw, split_ifs and maybe a few others from time to time so I am looking forward to reading the cheatsheet. You know about exact? and other tactics with ? appended.

Also you really need to be on top of the math in order to do the Lean (my experience at any rate).

[Anne Baanen]

Michael Rothgang said:

https://leanprover-community.github.io/mathlib-manual/html-multi/Tactics/All-tactics/#all_tactics is a list of all tactics in mathlib. It's automatically generated; I'm not sure how often it is updated automatically. (Anne Baanen Can you clarify this, or help me find out myself? Thanks!)

This is updated manually, typically for each Lean release. You can follow it here: https://github.com/leanprover-community/mathlib-manual

Generating a full and up to date list of tactics as part of doc-gen is one of my priorities. I have some prototypes already, I just need some time to see it through to the end and get something polished.

[Shreyas Srinivas]

I actually shared your frustration about the arbitrariness of tactics. They are essentially like a huge assembly language instruction set for proving things. So it is hard to get a grip on them.

So I am going to suggest something that is usually not suggested here: to work through the first 6-7 chapters of the book #tpil

I think the missing piece in your understanding of what lean is doing might be learning what those tactics are actually producing as a proof. This was my problem as well in other ITPs. It helps to work with some term level proofs before graduating to tactics.

[Dominic Steinitz]

And calc - really useful

[Anne Baanen]

Another of my priorities is to write good and consistent documentation for tactics that describe exactly what they can and cannot do. Not sure what the current Emacs plugin affords, but VS Code and Vim show tooltips with documentation when you put your cursor on a definition/tactic/keyword/...; the goal is to make all of those docstrings consistent with each other and as complete as practical.

[Weiyi Wang]

(deleted)

[Riccardo Brasca]

@Victor Miller Let me ask a more precise question: which proof do you prefer?

theorem foo1 : ∀ (a b : Nat), a.succ + b = (a + b).succ := by
  grind

theorem foo2 : ∀ (a b : Nat), a.succ + b = (a + b).succ := by
  intro a b
  rw [Nat.succ_add]

theorem foo3 : ∀ (a b : Nat), a.succ + b = (a + b).succ := by
  intro a b
  induction b with
  | zero => rfl
  | succ _ hb => rw [Nat.add_succ, hb, Nat.add_succ]

theorem foo4 : ∀ (a b : Nat), a.succ + b = (a + b).succ := fun _ =>
  Nat.rec rfl <| fun _ hb =>
    Eq.rec rfl <| Eq.rec (motive := fun (k : Nat) _ => _ = k.succ)
      rfl <| Eq.rec (motive := fun k _ => _ = k) hb rfl

theorem foo5 : ∀ (a b : Nat), a.succ + b = (a + b).succ := fun a =>
  Nat.rec (Eq.refl a.succ) <| fun b hb =>
    Eq.rec (motive := fun k _ => a.succ + b.succ = k) (Eq.refl (a.succ + b).succ) <|
      Eq.rec (motive := fun k _ => (a.succ + b).succ = k.succ)
        (Eq.refl (a.succ + b).succ) <| Eq.rec (motive := fun k _ => a.succ + b = k)
        hb (Eq.refl (a + b.succ))

[Snir Broshi]

(might be controversial but) I recommend Rocq's Software Foundations volume 1 (download link, chapter order, no lean port yet).
I think it introduces ITPs and tactics quite nicely, each chapter teaches you stuff in the comments and then gives you exercises, there's also a chapter about term mode ("ProofObjects").
I think the knowledge transfers to Lean quite nicely, though to work with Mathlib specifically is another level.

[Riccardo Brasca]

Those are proofs of the same statement (that for all natural number a and b we have a.succ + b = (a + b).succ. The last three proofs are "exactly the same", I just used less and less tactic. This is to show how one can write things more and more explicitly, controlling precisely what is going on. It's up to you to say which one is the best for you.

[Riccardo Brasca]

One can also use the equation compiler

theorem foo6 : ∀ (a b : Nat), a.succ + b = (a + b).succ
| _, 0 => rfl
| _, b + 1 => by rw [Nat.add_succ, foo6, Nat.add_succ]

[Victor Miller]

@Riccardo Brasca You said "Which proof do you prefer?". That depends a lot on my mood :-). This actually brings up another point: what is the basic axiomatic description of certain objects, like Nat? Your theorem is what, in Peano axioms, is the definition of addition. This makes me wonder what the underlying definition of Nat is in Lean. When I say, "my mood", it depends on what I'm interested in. I'd prefer the first if I just wanted to use Nat as a "Black box". The second almost seems tautologous. The fourth and fifth might be of interest if I wanted to understand how to manipulate proof objects (since this is the functional way).

[Marcin Pilipczuk]

I just want to chime in with sympathy. I was playing with Lean through Fall for a few hours per week and experienced the same frustration (except for the Emacs part, long term vim user here ;)). My answer current is to go back to the foundations, proofs with terms, programming with Lean and deeply understanding the core. I feel like without it I my understanding of what is going on was too shallow.

[suhr]

This actually brings up another point: what is the basic axiomatic description of certain objects, like Nat?

Logically it's just an inductive type. Like functions, it's not really axiomatic: you need not only typing rules, but also a computational rule.

But #print Nat.rec shows everything you need to know:

recursor Nat.rec.{u} : {motive : Nat → Sort u} →
  motive Nat.zero → ((n : Nat) → motive n → motive n.succ) → (t : Nat) → motive t
number of parameters: 0
number of indices: 0
number of motives: 1
number of minors: 2
rules:
for Nat.zero (0 fields): fun motive zero succ => zero
for Nat.succ (1 fields): fun motive zero succ n => succ n (Nat.rec zero succ n)

Rules show how recursor computes, for example Nat.rec motive z s Nat.zero computes to z.

[suhr]

Riccardo Brasca said:

Let me ask a more precise question: which proof do you prefer?

Let me add one more proof to the pile:

theorem foo7 (a: Nat): ∀ (b : Nat), a.succ + b = (a + b).succ :=
  Nat.rec (Eq.refl a.succ)
    fun b (hb: a.succ + b = (a + b).succ) =>
      show a.succ + b.succ = (a + b.succ).succ from
      congrArg Nat.succ hb

[Riccardo Brasca]

Victor Miller said:

Riccardo Brasca You said "Which proof do you prefer?". That depends a lot on my mood :-). This actually brings up another point: what is the basic axiomatic description of certain objects, like Nat? Your theorem is what, in Peano axioms, is the definition of addition. This makes me wonder what the underlying definition of Nat is in Lean. When I say, "my mood", it depends on what I'm interested in. I'd prefer the first if I just wanted to use Nat as a "Black box". The second almost seems tautologous. The fourth and fifth might be of interest if I wanted to understand how to manipulate proof objects (since this is the functional way).

You're right, Lean uses Peano's definition, but addition is defined by recursion on the second variable, so it's a+b.succ = (a+b).succ that is true by definition.

[Riccardo Brasca]

Anyway you can see everything by yourself: the declaration are called Nat and Nat.add. You can write #check Nat and ctrl+click on it to jump to the right file (in VS Code at least).

[Riccardo Brasca]

Each proof has it's own pro and cons:

• 1. it's fast but you don't know what is happening. It's good if you have to show this in a bigger proof and you don't care since it is mathematically stupid.
• 2. shows how things are written in the library
• 3. it's the mathematical "correct" proof, in the sense that it is reasonable to prove it like this if you are building the natural numbers, cf the NNG
• 4 and 5. are interesting if you want to understand what Eq.rec does, i.e. the definition of equality. Something you probably don't want unless you are into type theory.
• 6. interesting since it shows the equation compiler and structural recursion.

To fully grasp Lean you have to understand all of them, but you can also decide that you don't care at all about the definition of equality, or that you never want to use powerful tactic like grind.

[Riccardo Brasca]

If you want to avoid the recursor of the equality you can use ▸:

theorem foo7 : ∀ (a b : Nat), a.succ + b = (a + b).succ := fun _ =>
  Nat.rec rfl (fun b hb => Nat.add_succ _ b ▸ hb ▸ Nat.add_succ _ _)

[Riccardo Brasca]

In my opinion the best way to learn is to focus on one of the proofs, and learn as much as possible following that style (here I am only talking about proving theorems, if you want to write programs it is another story).

[Emily de Oliveira Santos]

Hey Victor! I've been trying to learn Lean since ~October, and really, really share your frustration here x_x. I've been on the fence about how serious I wanted to learn it until very recently — on and off flirting with the idea of getting to the point where I'd be able to get Real Work™ done with it.

I'm a very very new novice so please hold my advice very lowly compared to all the other people here, but:

• One thing that I've been finding helpful is working through The Hitchhiker's Guide to Logical Verification (LoVe).
• It's very CS-core but I think from your description this shouldn't be a problem.
• Whereas I struggled with too much stuff going on with Mathematics in Lean or Theorem Proving in Lean 4 and lack of understanding for stuff like the NNG, LoVe has indeed been lovely: it builds up things very very slowly, starting with types and how to construct terms for a few function types.
• There are still some points of frustration, but I think some of it is just inescapable with Lean :(
• I found going at it with a "Zen" attitude helps: expect it to take a long time, just try to understand as much as you can.
• I've also been finding using Claude Code to be extremely helpful. I'm asking it for feedback on my code after attempting exercises, leading to stuff like:

theorem Peirce_of_LEM_first_attempt :
    ExcludedMiddle → Peirce := by
  rw [ExcludedMiddle, Peirce]
  intro h_lem x y
  apply Or.elim (h_lem x)
  · exact (fun a ↦ (fun f ↦ a))
  · intro not_x f
    apply False.elim
    apply not_x
    apply f
    intro hx
    exfalso
    exact not_x hx

theorem Peirce_of_LEM_after_claude_feedback :
    ExcludedMiddle → Peirce := by
  rw [ExcludedMiddle, Peirce]
  intro h_lem x y f
  cases (h_lem x) with
  | inl hx  => exact hx
  | inr hnx => exact f (fun hx => absurd hx hnx)

(Of course one has to take Claude Code's advice with a grain of salt too, but I'd say it's at the very least certainly more helpful than unhelpful.)

I also found this nice for getting a better idea of which sources I can learn from: All Lean books and where to find them.

[James E Hanson]

Victor Miller said:

This actually brings up another point: what is the basic axiomatic description of certain objects, like Nat?

Something that's important to keep in mind when asking this kind of question is that type theory uses the word 'axiom' in a specific technical sense that isn't exactly compatible with the way the word is used in the rest of math. This can lead to what I consider to be misleading statements when people are trying to explain type theory to other people who aren't already familiar with it.

[James E Hanson]

The Peano axioms for the natural numbers, the group axioms, and Grothendieck's axioms for abelian categories are all not axioms in the sense of type theory.

[James E Hanson]

Anne Baanen said:

Not sure what the current Emacs plugin affords,

I am able to see at least the first line of documentation tooltips on Emacs. I don't know how to view the full thing, but that could be my fault.

[Tanner Duve]

Good to see you here Victor! As for your question about Nat, the type is defined as an inductive (an enum) in the usual axiomatic way - 0 : Nat and n : Nat -> S n : Nat (like List in Haskell with nil and cons). This is what allows you to do proofs by induction/programs by recursion on Nat

Most of the advice here has already been various book recommendations, but I'd like to second The Hitchhiker's Guide. It does a great job introducing both the tactic language and the core language from the ground up. Depending on what your goals are I'd recommend the first 4-6 chapters and follow it with something like #mil

[Kevin Buzzard]

Hey Victor!

I learnt Lean by hanging out with other people who were learning Lean and asking a ton of questions in (the 2017 analogue of) #new members . I use emacs for everything except Lean where I eventually bowed to the inevitable and switched to VS Code (to be honest, the main reason I switched was that I wanted to teach the software to students and I couldn't possibly tell 18 year olds to use emacs so I figured I should learn the software which I would be telling them to use).

[Victor Miller]

I’ve been trying to work my way through Alex Kontorovich’s RealAnalysisGame. I’ve been stuck for many hours (going on 6), with one of his early proofs. He’s trying to introduce tactics slowly, so one is restricted to a small list. I know what steps, even in excruciating low level details, I would use, but so far no dice. I even tried copying the problem into vscode but so far no luck.

[Snir Broshi]

Have you tried watching the lectures, or is it a problem not solved in class?

[Victor Miller]

Unfortunately watching the lectures on YouTube is interrupted every 5 minutes with ads. It’s excruciating.

[Richard Copley]

James E Hanson said:

I am able to see at least the first line of documentation tooltips on Emacs. I don't know how to view the full thing, but that could be my fault.

M-x eldoc RET should do it.

[Richard Copley]

Victor Miller said:

Unfortunately watching the lectures on YouTube is interrupted every 5 minutes with ads. It’s excruciating.

uBlock origin.