Lean or lean 4

Stream: general

[crab]

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

[crab]

I dont know if they said anywhere

[Arthur Paulino]

It's Lean 3

[Reid Barton]

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

[Arthur Paulino]

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]

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

[crab]

im looking forward to the port

[crab]

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]

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]

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

[crab]

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

[crab]

and mathlib is so amazing

[crab]

And the theorem proving capabilities are amazing

[crab]

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

[crab]

Or when im older

[Arthur Paulino]

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]

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]

Hmm

[Arthur Paulino]

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]

:) yes thank god to them

[crab]

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

[crab]

i would love to contribute one day tbh

[crab]

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

[crab]

or someone would have already been at me to it