Just starting, have project, need help

Stream: new members

[Daniel Flath]

LEAN community. I am a mathematician in Tucson, Arizona, USA. I am totally new to this group, with no experience at all with any proof assistant. I have a project that I want to formalize with LEAN. It's the Moebius problem. https://mathworld.wolfram.com/MoebiusProblem.html My work on it so far consists of hundreds of tiny lemmas, each of a similar nature. Before going ahead I would like assurance that errors have not crept in. Also I hope that after verifying what I have done with LEAN that perhaps an AI can find some patterns that I have not identified and help me continue.

How do you suggest I get started? I would probably need a LEAN experienced person to collaborate with me or at least help me get oriented and launched. Any takers? A "bring-your-own-project workshop" if such exists would be helpful.

Thanks in advance for you help and encouragement!

[Ruben Van de Velde]

When you say you have a lot of tiny lemmas, do you mean on paper or in lean?

[Daniel Flath]

I have them on paper, in Latex. My entire experience with LEAN is stage one
of the Natural Number Game.

[Ruben Van de Velde]

That's a good start - maybe #mil is a useful next step

[Daniel Flath]

Thanks! I will take a look at #mil
<https://leanprover-community.github.io/mathematics_in_lean/>