learning lean first time

Stream: new members

[crab]

I have never worked with a dependently typed language before, but I do have experience with f#. would it be hard to learn lean?

[Henrik Böving]

Lean will most definitely feel quite different from F# but you will probably have an easier time than say a person who only knows java and python since F# has quite few functional concepts and constructs you won't see in those languages but all the time in lean (e.g. tagged union types, lots of recursion, pattern matching etc).

[Arthur Paulino]

Hm, I think it depends on what you consider "hard". I had never worked with a dependently typed language or anything like F# before and I could say it's being "hard" for me. But since I enjoy the challenge (and the elegance of Lean), it's actually being "emotionally easy", so to speak... in the sense that I feel very motivated

[Arthur Paulino]

And, of course, I have to mention the supportive Lean community here on Zulip :heart:

[crab]

Henrik Böving said:

Lean will most definitely feel quite different from F# but you will probably have an easier time than say a person who only knows java and python since F# has quite few functional concepts and constructs you won't see in those languages but all the time in lean (e.g. tagged union types, lots of recursion, pattern matching etc).

tbh I use recursion, pattern matching and tagged union types in f# a lot

[crab]

im could say im comfortable with them

[Henrik Böving]

Exactly and that's your advantage over people who are not familiar with functional languages and will definitely help you with learning Lean.

[crab]

cool

[Julian Berman]

For me (a Python programmer) learning Lean has been way more difficult than I expected. I can imagine you indeed have quite a leg up there like Henrik said.

[Yaël Dillies]

My own data point is that learning Lean was quite demanding, although I never got stuck.

[Henrik Böving]

I found most of the language relatively easy to learn but that is most likely because I already had experience with Isabelle/HOL and Haskell so I had to adjust rather small parts of my mental model to fit with Lean.

[crab]

I find lean 4 much more begginner friendly and f#-like than lean3

[crab]

Tho lean4 doesn’t have mathlib and still pretty new

[Henrik Böving]

We do have a (very very) partial port of mathlib already over at https://github.com/leanprover-community/mathlib4

[crab]

That’s amazing

[crab]

if i were to use lean, i would definitely use lean4, but i would like to wait a bit

[Henrik Böving]

I'd say if you have never worked in a dependently typed language before you can already go ahead and start learning with Lean 4, it takes a time to get used to and the final (semi automatic) full port of mathlib to Lean 4 will also happen in the not so distant future, maybe by the time you know all the basics it will already have happened^^

[crab]

Why in lean4 did they decide to make the syntax much more friendly?

[Arthur Paulino]

What do you mean? It came after Lean 3 so it's an opportunity to improve

[crab]

Did the community want to introduce less experienced programmers?

[Alex J. Best]

What do you mean by friendly?

[crab]

Syntax wise

[Alex J. Best]

Please elaborate on specific changes you want to know about? Whitespace sensitivity? Lack of commas?

[crab]

No, the whole syntax in general

[crab]

I honestly find lean4 syntax much more beginner friendly than lean3

[Julian Berman]

Then what do you mean by "why" :)?

[Julian Berman]

Usually that would mean you think it's worse to do so.

[crab]

I honestly think that it was a very good move, but I want to understand the motive

[Julian Berman]

I suspect making Lean 4 more accessible to a wider set of programmers was an explicit goal -- early on Leo de Moura mentioned one of Lean 4's objectives was to become a good general purpose programming language

[Julian Berman]

making the syntax similar to other languages helps there

[Huỳnh Trần Khanh]

from a programmer's perspective, when legacy code is so ugly and hard to maintain you just want to throw everything away and rewrite from scratch. Lean 3 has a lot of "legacy cruft" (performance gotchas, "excessive memory consumption", etc) and the devs are fed up, so they make a totally new and better Lean :joy:

[Arthur Paulino]

Lean Together 2021: An overview of Lean 4
https://www.youtube.com/watch?v=UeGvhfW1v9M

[Huỳnh Trần Khanh]

everyone has been in this situation at least once

[crab]

The errors?

[Huỳnh Trần Khanh]

yes. these random errors are the worst. this is why the devs make Lean 4 instead :joy:

[Patrick Massot]

@Huỳnh Trần Khanh you should really show a lot more respect towards Lean developers.

[Huỳnh Trần Khanh]

I do. in fact, writing a theorem prover or a programming language implementation is a huge undertaking and even experts get things wrong

[Patrick Massot]

What have you accomplished to feel so much superior?

[Huỳnh Trần Khanh]

no, I'm just saying that Lean 4 is a much better version of Lean. I really respect the devs :heart:

[Arthur Paulino]

From what I've noticed (and I'm a newbie here), there is quite a lot more involved in the creation of Lean 4 than the mere workaround of bugs. The whole infrastructure is much superior, more generic and more powerful. We have a server that implements LSP, we have an FFI, we have a cleaner syntax.

And I'm certain that it's still just the tip of the iceberg

[Henrik Böving]

All metaprogramming related stuff has drastically changed (in a good way)

[Huỳnh Trần Khanh]

yeah. and persistent data structures, mimalloc and functional but in place are just so cool. Lean 4 even beats Haskell :joy:

[Martin Dvořák]

You say that Lean 3 didn't beat Haskell?

[Henrik Böving]

Lean 3 was not capable of beating Haskell performance wise, the Lean 4 devs did invest quite a lot of time and research into novel techniques to outperform it.

[crab]

Some time ago, when I looked at lean 3, I honestly felt discouraged, but lean 4 is so much more welcoming and exciting. The devs really accomplished a great task

[Huỳnh Trần Khanh]

probably tangential but I hope there will be no Lean 5, just like Python 3 is the final version of Python :joy: and ES6 is the final version of JavaScript :joy: I honestly hope that the strategy that the devs use to implement Lean 4 is the best one for Lean :laugh:

and also to people who think that I disrespect Lean devs: I don't :joy: in fact after I replied to Crab's message I was already typing something along the lines of Lean is a complicated system and implementing it is hard and stuff, I didn't want to come across as being rude :joy: every complicated piece of software has a rocky start and Lean is no exception lol

[Patrick Massot]

Huỳnh Trần Khanh said:

Lean 4 even beats Haskell

I don't think writing such sentences helps at all. You should compare such a meaningless sentence to what is written in Section 8 of https://arxiv.org/abs/1908.05647 for instance. There you'll see very specific benchmark presented in a very careful way, explaining why results should be interpreted with caution.

[Patrick Massot]

I know research can seem less fun that internet trolling, but this is what we do here.

[Mario Carneiro]

By the way, in case you weren't aware @Huỳnh Trần Khanh , that screenful of random errors (which everyone has probably seen before) is a symptom of memory exhaustion. When the memory allocator starts to say "no" to things, almost every activity lean tries to do will fail, but because it is a resilient program it keeps going and throwing more errors. It is unlikely that lean 4 changes this, memory exhaustion is an extremely difficult situation to recover from

[Mario Carneiro]

That's also why restarting lean usually fixes the issue, because it frees everything and starts over. It is unclear whether this is even fixable; if there is a memory leak then this would be the usual way users will encounter it but that implication goes only one way - you can also genuinely run out of memory, and if for example you have (accidentally or otherwise) attempted to compile all of mathlib in RAM that might be a significant possibility.

[Kyle Miller]

@Huỳnh Trần Khanh I was under the impression that a reason Lean 4 has new code isn't because the Lean 3 code base is somehow unmaintainable, but rather one of the goals of the project is self-hosting: Lean 4 is designed to be capable of writing Lean 4 in Lean 4.

[Huỳnh Trần Khanh]

isn't self hosting a rite of passage for programming languages? a self hosted compiler is a great indicator of a language's maturity right? that is, if the Lean compiler, a big, nontrivial application can be written in Lean itself that it means Lean is mature enough to tackle real life applications?

[Arthur Paulino]

I don't see that link very clearly, but it definitely displays a certain level of maturity. And I also find it extra helpful because we can learn a lot about Lean 4 just from reading Lean 4 source code

[Bernardo Meurer]

hi everyone, i've been having a lot of fun learning lean with game server, but i'm struggling to prove mul_pow, which led me to finally get fed up with the editor there.

i've set up my nvim with lean.nvim. is there any way I can play the game on my own editor? i don't know how to "set up" the lean file so that I can start proving theorem mul_pow (a b n : ℕ) : (a * b) ^ n = a ^ n * b ^ n := by, the game doesn't teach that.

[Kevin Buzzard]

Are you aware of "typewriter mode"?

Screenshot from 2025-12-20 02-08-29.png

You can just go into a free-form input mode there. But if you want fancy nvim keyboard shortcuts or whatever then you can just clone the repo https://github.com/leanprover-community/NNG4 and run it locally.

[Bernardo Meurer]

oh the syntax is a little different huh

[Bernardo Meurer]

before i would do induction n with i hi, in neovim on that repo it wants me to use | after the newline

[Kevin Buzzard]

oh I think I hacked the induction tactic in NNG4

[Kevin Buzzard]

You can see all the dirty secrets here https://github.com/leanprover-community/NNG4/tree/main/Game/Tactic

[Bernardo Meurer]

ohhhhhhh

[Kevin Buzzard]

In the usual editor mode you can't do multiline input so the | approach in Lean 4 was no good for me

[Bernardo Meurer]

okay, just need to adapt a little bit, no problem

[Bernardo Meurer]

fwiw, i'm finding this a wonderful game, this is the first thing that has pried me away from crossword puzzles

[Bernardo Meurer]

i found mul_pow hard, i tried to use claude in "teacher mode" or w/e it's called but it's just way too nice and gives it right away :(

is it okay to ask for hints here?

[Kevin Buzzard]

Sure

[Kevin Buzzard]

For mul_pow I would do induction on n but I can see it will be a bit painful, especially because you are kind of crippled in NNG because you don't have the tools which will manipulate (a^n * a) * (b^n * b) into (a^n * b^n) * (a * b) easily so you might have to manually do it

[Kevin Buzzard]

import Mathlib

example (a b c d : ℕ) : (a * b) * (c * d) = (a * c) * (b * d) := by
  rw [Nat.mul_mul_mul_comm]

example (a b c d : ℕ) : (a * b) * (c * d) = (a * c) * (b * d) := by
  ring

example (a b c d : ℕ) : (a * b) * (c * d) = (a * c) * (b * d) := by
  grind

etc etc (this is in real Lean, not NNG)

[Kevin Buzzard]

The model solution is pretty inelegant

[Bernardo Meurer]

oh, so maybe i was giving up too easy, it was always looking really gnarly and i thought "it can't be this i gotta be going in the wrong direction"

[Bernardo Meurer]

i guess i can make a pr adding a hint that it looks gnarly :P

[Bernardo Meurer]

oh, it resolves trivial goals for me! i don't need to write rfl after! neat!

[Kevin Buzzard]

Oh yeah I hacked rw as well because beginners found it confusing

[Kevin Buzzard]

That was back in the day when x + 0 = x could be proved by rfl (before we changed that too in NNG). I should say that I keep saying "I" but actually several other people were doing the dirty work of writing the meta code, I just designed the levels

[Bernardo Meurer]

theorem mul_pow (a b n : Nat) : (a * b) ^ n = a ^ n * b ^ n := by
  induction n with
    | zero =>
      repeat rw [pow_zero]
    | succ n ih =>
      repeat rw [pow_succ]
      rw [ih, ←mul_assoc,← mul_assoc, mul_assoc (a^n) (b^n) a, mul_assoc (a^n) a (b^n), mul_comm (b^n)]

ta-daa!

[Bernardo Meurer]

i wish there was one of these for real analysis, that would be fun

[Chris Henson]

Bernardo Meurer said:

i wish there was one of these for real analysis, that would be fun

You're in luck, one was recently created! See https://adam.math.hhu.de/#/g/alexkontorovich/realanalysisgame

[Bernardo Meurer]

awesome!

[Bernardo Meurer]

man, i am really finding the maxim that "computer scientists are mathematicians who can only prove things by induction" to be true :P

[Julian Berman]

I would love to have a better story for playing lean4game-based games in lean.nvim someday, but there isn't one better than Kevin's suggestion quite yet.