Luiz Carlos Rumbelsperger Viana

Stream: new members

[Luiz Carlos Rumbelsperger Viana]

Hello all, new member here, first time getting to know Zulip. Just introducing myself.

I have pretty much 0 experience with online forums of any sort, but I have been programming in Lean for some time now. My latest achievement is a proof of the soundness of classical predicate logic. Then, since some questions about the language have piled up with time, I decided to start being more sociable.

I am also a computer science undergraduate student at PUC Rio, studying type theory and logic under Professor Edward Hermann Haeusler.

So anyway, I suppose that 's it, what should I do next?

[Jalex Stark]

If you want to learn stuff, this is a list of resources
https://github.com/leanprover-community/mathlib/wiki/Where-to-start-learning-Lean

[Jalex Stark]

When I first came here, I found it pretty fun an informative to read a bunch of old conversations

[Jalex Stark]

if you have questions you should ask them, probably here in the new members stream. Try to make one "new topic" per logically distinct question. By that I mean something like: try to make it so that anyone who is curious about the first post in the topic will probably want to read the entire conversation that follows

[Jalex Stark]

If you have projects, you should say more about them here. People can give you advice or point you to similar projects that are already done, or tell you that your project is exciting enough to go in mathlib if completed

[Luiz Carlos Rumbelsperger Viana]

Hey, thanks for the response, I checked the link now. I had already read most of TPiL and often use it and Logic and Proof as a reference, but I didn't know about Codewars, so thanks.

I suppose I am going to ask a technical question in my next topic then.

As for projects, currently I have some exercises about predicate logic to finish which I hope to write in a way that is instructive enough to be read by another human being, for teaching logic using Lean and such. When I finish them, maybe I will make a tutorial or something.

[Kevin Buzzard]

If you make a mini project which you don't plan to PR to mathlib then just make sure it compiles, make a nice README and dump it on GitHub and tell people about it. There will be folk who are interested.

[Kevin Buzzard]

And then make another project :-) You can learn this language by doing and although we're not yet at the stage where you can Google if you get stuck, asking here is very effective

[Matt Earnshaw]

I would certainly be interested to look at your soundness proof if you were willing to share

[Luiz Carlos Rumbelsperger Viana]

@Matt Earnshaw , I am sorry I took about a week to answer this, I was quite busy this week.

So after adding some minor edits, I went and made the project public: https://github.com/maxd13/logic-soundness.

Check it out.

[Matt Earnshaw]

Luiz Carlos Rumbelsperger Viana said:

Matt Earnshaw , I am sorry I took about a week to answer this, I was quite busy this week.

So after adding some minor edits, I went and made the project public: https://github.com/maxd13/logic-soundness.

Check it out.

great, thank you!

[Luiz Carlos Rumbelsperger Viana]

Matt Earnshaw said:

Luiz Carlos Rumbelsperger Viana said:

Matt Earnshaw , I am sorry I took about a week to answer this, I was quite busy this week.

So after adding some minor edits, I went and made the project public: https://github.com/maxd13/logic-soundness.

Check it out.

great, thank you!

Please give me some feedback later.