Zulip Chat Archive

Stream: general

Topic: Lean or lean 4

crab (Jan 22 2022 at 18:05):

Is this video using lean or lean 4? https://youtu.be/b59fpAJ8Mfs

crab (Jan 22 2022 at 18:05):

I dont know if they said anywhere

Arthur Paulino (Jan 22 2022 at 18:06):

It's Lean 3

Reid Barton (Jan 22 2022 at 18:06):

Probably because Lean 4 did not really exist at the time.

Arthur Paulino (Jan 22 2022 at 18:09):

Mathlib has changed since then and some declarations used on that video have changed as well. Check this thread if you're intending to reproduce that proof

crab (Jan 22 2022 at 18:26):

Mathlib has like every single function i would ever need in my life

crab (Jan 22 2022 at 18:26):

im looking forward to the port

crab (Jan 22 2022 at 18:27):

Would i need to be some sort of mathematician or be really good at math to be doing theorems. I really want to do them, but i dont know how i would implement them in lean. Also, im terrible at proofs and logic

Henrik Böving (Jan 22 2022 at 18:32):

Being at least okay with proofs and logic is certainly a requirement for doing proofs in Lean as well. Regarding being good with mathematics, sometimes when mathematicians here have a question I can at least somewhat understand what is happening on the Lean level but in the majority of cases I lack the math knowledge to actually help so if you want to contribute to mathlib itself I feel like you need to at least know more mathematics than I do (which is not that much to be fair :P).

crab (Jan 22 2022 at 18:36):

I’m probably one of the youngest here. I honestly was curious about lean for general programming, which im gonna use

crab (Jan 22 2022 at 18:36):

but sometimes my general programming is using it to help me with math

crab (Jan 22 2022 at 18:36):

and mathlib is so amazing

crab (Jan 22 2022 at 18:37):

And the theorem proving capabilities are amazing

crab (Jan 22 2022 at 18:37):

So i thought i would at least do some theorem proving in lean

crab (Jan 22 2022 at 18:37):

Or when im older

Arthur Paulino (Jan 22 2022 at 18:42):

I would refrain from stating sentences like

Also, im terrible at proofs and logic

Proofs don't need to be about mathematical objects like functors and algebras. You can have proofs about, say, the consistency of a certain data structure you're building. I will give you an example.

Suppose you've built a function that inserts a natural number into a list of natural numbers in such a way that you'd expect the characteristic of being "in ascending order" not to be lost.

Then you can have a proof that this function creates an "ascending list" off of an empty list, regardless of the number you insert. You can also have a proof that, given an ascending list, your function keeps the resulting list in ascending order too. Then you can have a proof that, starting from an empty list, no matter how many times you apply your function, the resulting list will be in ascending order. At this point you should be pretty confident about the correctness of your function.

Arthur Paulino (Jan 22 2022 at 18:46):

Notice that if I give you the challenge of building such function, you'd likely be capable of coming up with it pretty quickly. So somehow you do have the intuition for the proofs I mentioned.

crab (Jan 22 2022 at 18:50):


Arthur Paulino (Jan 22 2022 at 18:54):

Some people are talented, no doubt about that. But others (like myself) can be trained/taught. Thank god talented people exist to show us the way :smiley:

crab (Jan 22 2022 at 18:58):

:) yes thank god to them

crab (Jan 22 2022 at 19:02):

imo, the most talented people are the people who created and are currently creating lean

crab (Jan 22 2022 at 19:02):

i would love to contribute one day tbh

crab (Jan 22 2022 at 19:08):

But I feel like by the time I would contribute to Mathlib, there would be nothing to contribute lol

crab (Jan 22 2022 at 19:09):

or someone would have already been at me to it

Last updated: Aug 03 2023 at 10:10 UTC