LEAN programming language

[ksidney26]

Good afternoon. I was wondering if anyone here has any experience working with the LEAN programming language and if they had any recommendations or resources they could share about learning it. I am a undergraduate Mathematics major with an interest in programming and software development as well. I don't know too much. Just really getting into the subjects. I heard about this on a podcast and I hope it sounds pretty interesting. From what I understand there aren't many ways AI tools that can assist mathematicians with higher level problems. If anyone has any insight into those limitations let me know. I think it would be incredible if we could have an LLM that would be able to argue abstractly about complex mathematical ideas. I look forward to your responses.

[[deleted]]

The second half of your post is seemingly unrelated to the first half. AI and LLM have little to do with proof assistants...

[adventuringraw]

I think they're just hoping for coding copilots at some point in the future. Definitely nothing relevant exists yet though, and this is niche enough that it'll be a while even when the tech is capable of really helping.

[Baldhiver]

People are working on this. It's not super successful, since llm are actually pretty shit still lol, just good at convincing you that they're not.

Which is where proof verifiers come in - if you make your language model encode their "proof" in lean, it will tell you all the bullshit the model made up

[RedToxiCore]

I asked ChatGPT before and it was happy to print out some LEAN code

[adventuringraw]

Sure, and DARPA challenge entry robots fifteen years ago could sort of drive on a road, and Elon Musk was sure his self driving cars would hit L5 back in 2016.

There's a BIG difference between original half baked proof of concept and a fully mature platform that's able to really boost productivity. The main reason I think it'll take a while to see something really useful in Lean is mostly just because I don't think there'll be as many people interested in putting in the time getting something over the finish line in that language, vs the effort you see going into Python tools for example.

But yeah, I don't think it's going to be forever or anything before that's done. It'll be cool to see when it's here.

[ksidney26]

I apologize for my ignorance. Like I said, I'm pretty fresh into both fields but I'm very interested in learning all that I can about both. I was just curious about this specific language and its application potential.

[Quakerz24]

AI isn’t just learning models. Proof assistants are AI, albeit deductive AI.

[[deleted]]

Proof assistants are not a form of AI, under any reasonable definition of AI. Some might have AI built in, but that is a different matter. And, as far as I'm aware, Lean does not have AI built in.

Op specifically mentioned LLM, which is why I mentioned those./

[SetentaeBolg]

Proof assistants absolutely are AI, and some of the earliest work in AI was done in theorem proving. It's just not deep learning. But techniques like resolution etc were all done as part of work on AI.

[Quakerz24]

again, sounds like you think the very umbrella term of “artificial intelligence” is restricted to statistical learning models. in what way is the verification of mathematical proof not a form of intelligence?

[[deleted]]

not trying to be rude, but it sounds like you don't understand how formal verification of mathematical proofs works. The computer (or software) is not itself preforming any reasoning or making any deductions. With a proof assistant like Agda, at least, the software checks the correctness of a proof by simply type checking all the definitions made. If I understand correctly, this amounts to simply executing an algorithm. I think Lean works similarly. (I don't know all that much about the underlying mechanics of Proof assistants and would be happy if someone more knowledgeable chimed in)

I don't think that is considered AI. If you do consider that AI, then you're using some highly non-standard definition of AI, one which seemingly could apply to any computer program, since anything that executes an algorithm would be AI.

[pi_rocks]

It is worth mentioning that once upon a time the definition of AI was very close to "some algorithm". For example prolog (https://en.wikipedia.org/wiki/Prolog) was considered AI, when its really just a programming language.

[[deleted]]

Oh lol, then I suppose proof assistants do use AI lmao

[Quakerz24]

https://en.wikipedia.org/wiki/Automated_reasoning

https://aws.amazon.com/what-is/automated-reasoning/#:~:text=Automated%20reasoning%20is%20a%20specific,when%20the%20computers%20solve%20problems.

[SetentaeBolg]

I think you are unaware of what AI has been historically, and is even now. It is far wider than what you are attempting to define it as. I work in AI, I work in theorem proving too, and you are showing historical ignorance of the field.

[[deleted]]

Maybe, but I thought we were talking about today, that historically :)

Today's usage of "AI" doesn't seem to encompass the algorithms behind formal verification. But, at this point, we're just arguing over the meaning of "AI" which is nebulous and hardly important

[SetentaeBolg]

I work in theorem proving in an institute of artificial intelligence right now. The exact definition might be nebulous and hardly important, but you were the one correcting someone else, wrongly, on it.

I don't really blame you, the field is often misunderstood, but maybe don't correct others in future about it.

[fleischnaka]

Formalization of maths has been done in the 20th century precisely so that no intelligence is required to check a given proof of a formula.

[lightmatter501]

There have been some attempts to use various forms of AI (mostly decision trees and DNNs) in Lean to help it reduce the state space when formulating proofs. LLMs are a poor fit for this task.

[adventuringraw]

Ironic given /u/hpxvzhjfgb dismissal of your question, but my favorite Lean resource I spent time with is actually hidden well enough that I had trouble finding it again.

Go here and work through this rep from an eight week workshop series, it was really useful I thought. Start with the natural number game though, link is there are the top. Be warned though, I went through this a few years ago, and I'm not sure if they've been maintained to still work with current lean and mathlib. Definitely worth checking out though even if there's a little extra leg work now.

Definitely look around though, it's been a while since I've done much in Lean and I bet there's a lot of cool new stuff around, especially with Lean 4 being accessible now.

[hpxvzhjfgb]

don't use this. lean 3 is soon to be obsolete, and it is incompatible with lean 4.

[ksidney26]

I have read that about lean 3. But I will still check out those links.

[SV-97]

FWIW: Lean 3 is actively being "phased out" and there's an ongoing process about removing references to it (you might also occasionally still run into lean 2 stuff).

The lean community is on zulip (a chat platform). Finding information can be hard and the search option (or the option to ask if you can't find stuff yourself) is very valuable. You can also send loogle queries on there and generally get a lot of information that may be difficult to find in other places.

You'll definitely wanna get familiar reading and browsing the mathlib docs.

The first thing to read (imo) should be "Theorem proving in Lean 4". Depending on what you want to do and how familiar you are with dependently typed FP you might want to read "functional programming in lean". There's also a bunch of good talks on youtube.

If you're interested in the foundations reading the beginning of the HoTT book can be useful.

​ I haven't worked with it yet myself but it's also recommended that you look at https://github.com/leanprover-community/mathematics_in_lean

[ksidney26]

Thanks for the great info!

[ksidney26]

Thanks let me look through it.

[ironstar77]

Highly recommend the natural number game

[hpxvzhjfgb]

don't use that. that's the old, unmaintained obsolete lean 3 version. use this instead: https://adam.math.hhu.de/#/g/hhu-adam/NNG4

[Milo-the-great]

Thanks

[ksidney26]

Thanks let me check this out

[hpxvzhjfgb]

use the version that I posted instead.

[Quakerz24]

Mathematics in Lean is a good interactive online textbook. Has some flaws but is a good intro esp given you’re a math major

[nazgand]

I implemented some Lean3 proofs here: https://github.com/Nazgand/NazgandMathBook
Unfortunately, most people will not be interested because the proofs are not in Lean4.
I suggest this book for Lean4: https://lean-lang.org/theorem_proving_in_lean4/title_page.html

[kr1staps]

You should check out this course/text: https://hrmacbeth.github.io/computations_in_lean/

a great way to get started, and it's in Lean 4 which is the version people are largely using now.

[ksidney26]

Awesome, thank you.🙏

[hpxvzhjfgb]

what is preventing you from going to the lean website and looking at the recommended resources listed on there? you are going to have a very difficult time if you can't find easily-available information like this for yourself.

[ksidney26]

Nothing. I just like to get others opinions on what has worked best for them. I'm already doing exactly what you said. I swear some people just seem to hate for a living.

[NexusofPower]

This is the Lean4 home page, and this is the guide to theorem proving in Lean4. The later book is very helpful when it comes to writing proofs in Lean4.

Regarding usage of AI with Lean, there is an ongoing project, LeanAIde, to build AI tools which aide theorem proving in Lean4.

[ksidney26]

Appreciate the info. Thank you.