To work on a project

Stream: new members

[İmran Tanq]

Hello, I want to work on a new project. Actually, I’ve never worked on any project before, and now I want to start, but I’m not exactly sure how to find a project. Could you explain exactly how to find a new project?

[Yaël Dillies]

Welcome! Do you mean a collaborative project or a project to work on your own? What are your (mathematical) interests?

[İmran Tanq]

For now, it might be better if I work on my own. My main interests in mathematics are analysis and algebra, but I can quickly adapt to other areas as well.

[Kenny Lau]

do you essentially want someone to say, here's a gap in algebra, go formalise this?

[Kenny Lau]

because if so you can try to go through Atiyah-Macdonald and find the first result not in mathlib

[İmran Tanq]

How can I check the theorems in the book against Mathlib? How can I know whether a theorem is already in Mathlib or not?

[Kenny Lau]

https://www.leanexplore.com will help you a lot

[Kenny Lau]

give me an example from the book and i'll show you how it works

[İmran Tanq]

For example, let's take the second proposition on the first page of the book.
How can we check it in the archive?

[Niels Voss]

If your end goal was getting this into mathlib and you want to make sure you aren't duplicating work, then you probably want to ask in #**Is there code for X? . There might also be some people working specifically on formalizing Proofs from THE BOOK (I recall some discussion about it a while ago but don't know the status) (nevermind, I misread the above conversation)