new user wanting to use lean4 for set theoretic proofs/simpl

Stream: new members

[Pete]

I would like to know perhaps as example file, how I could
(a) simplify set theoretic expressions involving intervals
(b) prove equivalence between two set theoretic expressions

[Eric Wieser]

Can you phrase each question in terms of an example with an #mwe (with statements but no proof) ?

[Pete]

#nvmd

[Ruben Van de Velde]

Did you read #mwe? It's a link

[Pete]

yes have you that i am a new user? It's an info that i hardly am competent to run test files.
look, i find it already difficult to navigate the documentation provided , which is sub par in terms of providing mwe to simply run in order to figure out whether the installation of lean4 works.

[Ruben Van de Velde]

Sure. I'm just suggesting that you get more answers if you ask them in a way that is easy for people to answer

[Pete]

i understand, i hope you equally understand that i am trying my best by providing an explicit example that any mathematician would understand. and by doing so be pointed out to potential examples that have already been done via lean4 and are related to my question. do u also see what i am saying?

[Jireh Loreaux]

@Pete you can use $\LaTeX$ here by wrapping in (two) $$. Editing your previous post with that would at least make it readable if you can't make a mwe.

[Jireh Loreaux]

Also, do you know that you can get a playground in Lean online for free? The link is here: https://live.lean-lang.org . Typing import Mathlib at the top of that will give you access to the entirety of the library.

[Notification Bot]

This topic was moved here from #lean4 > new user wanting to use lean4 for set theoretic proofs/simpl by Yury G. Kudryashov.

[Yury G. Kudryashov]

@Pete I moved your question to a more appropriate stream.

[Kevin Buzzard]

Pete, the point is that there can be many ways in Lean to say one thing in mathematics, so to remove ambiguity the community here likes people to ask their questions by posting Lean code. This is a good way to avoid miscommunication.

[Pete]

Jireh Loreaux said:

Pete you can use $\LaTeX$ here by wrapping in (two) $$. Editing your previous post with that would at least make it readable if you can't make a mwe.

Thanks for being pedantic i suppose , and thanks for this immense help on this, clarifying that i should not use lean coz community has obvious issues and challenges. definitely not a way to welcome new user.

[Pete]

.

[Pete]

Yury G. Kudryashov said:

Pete I moved your question to a more appropriate stream.

that's very helpful coz i dont know where it was moved to.

[Pete]

Kevin Buzzard said:

Pete, the point is that there can be many ways in Lean to say one thing in mathematics, so to remove ambiguity the community here likes people to ask their questions by posting Lean code. This is a good way to avoid miscommunication.

Kevin, thanks i understood that this forum is not for completely new users. that's all i really understands. thanks for taking the time to illustrate this point.

[Kevin Buzzard]

@Pete Maybe you want to start with Mathematics In Lean https://leanprover-community.github.io/mathematics_in_lean/index.html , this will give you some idea about basic usage of the software. You can't run before you can walk, and the software has a steep learning curve. Section 4 is about sets.

[Kevin Buzzard]

There is also the set theory game https://adam.math.hhu.de/#/g/djvelleman/stg4

[Yury G. Kudryashov]

Pete said:

Yury G. Kudryashov said:

Pete I moved your question to a more appropriate stream.

that's very helpful coz i dont know where it was moved to.

It was moved to the #new members stream. Since you're replying in this stream, you've managed to find it. I tagged you after moving so that you get a notification and can jump to the new location.