Zulip Chat Archive

Stream: new members

Topic: How long to learn Lean?

Alex Altair (Oct 03 2023 at 00:03):

I'm curious to hear people's intuitions for how long it takes to learn Lean. To make this question more constrained, let's say the person is a senior math major, and they're comfortable with at least one programming language (but not a functional language). How long would it take before they could use Lean to, for example, verify that their homework proofs are correct?

Patrick Massot (Oct 03 2023 at 01:49):

Nobody can answer this question. It depends on people, on how much effort is put into learning and on the homework.

Jesse Slater (Oct 03 2023 at 02:11):

If you want the perspective of another math student, I can give my experience. I spent a couple of months of fairly regular self study reading the books last year. I have the prior experience of being a computer science student as well, so I have a fair amount of experience with functional programming. I was able to get the basics down, but still found writing proofs to be very hard. Now I have just done the first month of a college class studying Coq, and now I am starting to get a good handle on writing proofs. I don't think I would be able to verify most of the proofs I do in math classes though, without a suggnificant amount of extra work.

I found it very hard to self study, and don't think I would have made much more progress without a class structure. You may have a different experience, but I would recommend looking for a set of lectures. Also, I would recommend the Software Foundations series of textbooks from UPenn. Its free online and covers Coq, which is very similar to Lean. Coq is much older, so the resources online are more developed, so studying it might be a good place to start.

Good luck on your journey!

Patrick Massot (Oct 03 2023 at 02:16):

The Software Foundations series of textbooks is known to be fantastic if you want to learn software verification but it is completely irrelevant for mathematics.

Bulhwi Cha (Oct 03 2023 at 02:56):

I'm a university dropout and don't know how to program. I've read only some part of math textbooks before. It took me more than 300 hours to read #tpil and solve all exercises in the book.

Theorem Proving in Lean 4

  • Jan 2022–Feb 2023, 11 months of learning
  • Translated 498 terms into Korean
  • Note 1: I estimated times spent reading Chapters 3 and 4 at 20 h and 23 h, respectively; times spent translating terms in these chapters at 6 h 45 min and 6 h, respectively.
  • Note 2: times spent reading other materials, such as core Lean files, are included in the “Reading the text” activity.
Activity Time ([h]:mm)
Reading the text 236:20
Translating terms 64:10
Solving exercises 73:05
Total 373:35

Times spent for each chapter of TPiL

Kevin Buzzard (Oct 03 2023 at 05:29):

I started in summer 2017 and created a self-study program where I read #tpil and did all the exercises, then formalised about 100 problems in very basic 1st year undergraduate mathematics (and asked a ton of questions on the Zulip) and then I formalised the definition of a scheme as a group project. Six months later in winter 2017 I felt I was competent. This process could definitely be streamlined now though because back then there were no teaching materials for mathematicians other than #tpil .

Somo S. (Oct 03 2023 at 08:36):

@Patrick Massot said:

The Software Foundations series of textbooks is known to be fantastic if you want to learn software verification but it is completely irrelevant for mathematics.

I have no interest whatsoever learning Coq, but I am interested in learning about software verification. I have about been studying lean for pretty much full time since March .. If the Coq material in SF is self contained (i.e. I do not need to pick up some other book/resource to learn Coq before studying SF), I would be willing to study SF. Is SF self contained in that way?

Shreyas Srinivas (Oct 03 2023 at 09:23):

Somo S. said:

Patrick Massot said:

The Software Foundations series of textbooks is known to be fantastic if you want to learn software verification but it is completely irrelevant for mathematics.

I have no interest whatsoever learning Coq, but I am interested in learning about software verification. I have about been studying lean for pretty much full time since March .. If the Coq material in SF is self contained (i.e. I do not need to pick up some other book/resource to learn Coq before studying SF), I would be willing to study SF. Is SF self contained in that way?

It is.

Alex Altair (Oct 03 2023 at 14:27):

Kevin Buzzard Nice! Was that six-month period more like full-time Lean study or part time?

Alex Altair (Oct 03 2023 at 14:29):

@Bulhwi Cha Love how much data you took on that, thanks for sharing!

Utensil Song (Oct 03 2023 at 14:42):

I don't think one should spend too much time to "learn" Lean. I did read Lean manual, #tpil, #mil, #fpil, #tmop for Lean 3 and Lean 4 etc. and major Lean papers, spent quite some time to fight with some exercise proofs to get to the bottom of them. The time is way less than months, basically just weeks in part time. But these are only the starting point. I've learned much more from chats on Zulip about solve different levels of problems, and reading source code of many Lean projects, usually with a question "how to do X in Lean (idiomatically)?", that's also the most time-consuming part, proportional to the reward. (Well, I don't claim to know Lean, as I believe it's more of a life-time endeavor, frankly so far I can only use Lean to do a fraction of what I want to do)

As for "How long would it take before they could use Lean to, for example, verify that their homework proofs are correct?", this greatly depends on the homework. One (that "is a senior math major, and comfortable with at least one programming language") can already do this halfway through #tpil if they make good use of the materials known to them at that time. But if the homework touched topics that the whole community hasn't been working on, it could be way harder than just finishing reading books and doing exercises and even asking on Zulip, since it might involve new ways to do math in Lean, or knowing how to properly ask that question with a #mwe .

Arthur Paulino (Oct 03 2023 at 14:55):

I would say that "learn Lean" is a pretty wide gate. There are many layers to it.

For example, one can use Lean 4 as a programming language and end up facing pretty much none of the real challenges involved in formalizing mathematics.

Now, if you're referring to using Lean 4 as a theorem prover specifically, part of it may be broadly summarized as "learning the by DSL", which includes understanding tactics. But you'll need just enough type theory so you can understand definitions, create your own and state your theorems.

And there's the metaprogramming approach, which allows you to extend the by DSL, create your own custom commands and much more.

Alex Altair (Oct 03 2023 at 15:48):

@Utensil Song Curious if you have any examples in mind for topics that the community hasn't been working on

Alex Altair (Oct 03 2023 at 15:50):

@Arthur Paulino Nice, I like that breakdown between learning Lean qua programming vs theorem proving vs metaprogramming. (I'm personally interested in the theorem proving branch, though happy for this question to serve as a place for people to give answers to the other parts too)

Kevin Buzzard (Oct 03 2023 at 16:55):

Alex Altair said:

Kevin Buzzard Nice! Was that six-month period more like full-time Lean study or part time?

Oh I had a full time job throughout that period, this was evenings and weekends, although it became somewhat of an obsession (and still is)

Kevin Buzzard (Oct 03 2023 at 16:57):

PS to Somo S: as part of my 6 month induction process I worked through a bunch of material in the first volume of SF, just translating it directly into Lean and solving the exercises, and I could do this with very little background (I was doing it right at the start of my learning process). But it was so far from the kind of stuff I was interested in that I moved onto undergraduate problem sheets from my own intro to proof class.

Martin Dvořák (Oct 03 2023 at 18:46):

At the beginning, I was playing NNG and solving tutorial exercises. I had no major problems there — these exercises were designed to be easy.

When I started working on my own projects, I was getting lost all the time. I was free to write definitions however I wanted, and I could set my own goals (both in the literal and abstract sense). I was not able to handle such an amount of freedom. I eventually managed to write my definitions correctly (w.r.t. the informal definitions, not necessarily in a Lean-and-mathlib-friendly way), but proving stuff was a real issue — I knew I was supposed to look beyond the tools I was using when solving beginner exercises, but there was "too much out there". I ended up using many tools in a very suboptimal manner. Almost everything was a footgun in my hands at that time.

My progress wasn't smooth, but the experience was pretty rewarding. There were moments when certain things just clicked and I could suddenly see that "I can do this kind of easy things with ease". Overall, it took me about half year of full-time study to reach a point when my projects started to have a direction and my proofs stopped feeling like eventually deleting most of the lines I wrote.

Right after finishing ITP paper, I switched to Lean 4. There was a transition period during which I was temporarily very clumsy again and during which the syntax of Lean 3 was creeping into my Lean 4 code. It took me about a month to get somewhat comfortable again. However, I believe I am now slightly more fluent in Lean 4 than I ever was in Lean 3.

Kevin Buzzard (Oct 03 2023 at 19:12):

You should try the last level at https://adam.math.hhu.de/#/g/hhu-adam/NNG4 , that's not designed to be easy :-)

Henrik Böving (Oct 03 2023 at 21:11):

Kevin Buzzard said:

You should try the last level at https://adam.math.hhu.de/#/g/hhu-adam/NNG4 , that's not designed to be easy :-)

image.png
cant make it :P

Kevin Buzzard (Oct 03 2023 at 22:00):

@Alexander Bentkamp . Henrik you probably need to clear your cache, unfortunately.

Alexander Bentkamp (Oct 04 2023 at 06:03):

@Henrik Böving ideally, send me the content of your local storage before you delete it.

Henrik Böving (Oct 04 2023 at 06:08):

Too late for that already I'm afraid :(

Henrik Böving (Oct 04 2023 at 06:08):

But it did help^^

Utensil Song (Oct 04 2023 at 18:00):

Alex Altair said:

Utensil Song Curious if you have any examples in mind for topics that the community hasn't been working on

To name a few that would be challenging:

Not that no one is working on them, but few are working/exploring on them, or the work could be paused anytime, or how to approach them remains an open question, unlike certain topics that have a group of experts working on and are continuously evolving, based on some established design.

Ming Li (Oct 06 2023 at 13:37):

I am reading GimpseOfLean and MIL. How can I tell what depends on tactics of the two books but not of mathlib4?

Patrick Massot (Oct 06 2023 at 15:27):

Those have no specific tactics.

Ming Li (Oct 07 2023 at 02:02):

I moved the file Basic.lean of GlimpseOfLean to Mathlib4. Why does the part after "Open BigOperators" cause some error?

Patrick Massot (Oct 07 2023 at 02:58):

It is because of incompatible option. You can add set_option autoImplicit true somewhere near the beginning of the file.

Patrick Massot (Oct 07 2023 at 02:59):

This option enables a cool feature of Lean 4 which can be a bit confusing. After a lot of discussion, people temporarily decided to switch it off in mathlib.

Patrick Massot (Oct 07 2023 at 03:00):

You may also find a couple of lemma in that file that have been recently incorporated into mathlib, so Lean will complain. I will update GlimpseOfLean when I'll have time. But none of this is about new tactics.

Ming Li (Oct 07 2023 at 03:18):

It did solve my concern in big time. Thanks a lot.

Ben Nale (Oct 09 2023 at 06:44):

I just played the natural numbers game in a few hours and learned Lean :). So to answer your question, it takes a few hours.

Kevin Buzzard (Oct 09 2023 at 07:58):

NNG doesn't teach you how to make structures or how to use the typeclass inference system. Those I learnt after doing a maths project myself.

Last updated: Dec 20 2023 at 11:08 UTC