I want to second this. I started working on a project in Lean only last December. Since then, I've made several contributions to the mathlib github repo - the f

I want to second this. I started working on a project in Lean only last December. Since then, I've made several contributions to the mathlib github repo - the first time I've contributed to open source despite wanting to get into it for a few years. The Zulip forum https://leanprover.zulipchat.com/# https://leanprover.zulipchat.com/# is very welcoming and responsive to questions. If you're interested in mathematics and you want to contribute to the growing hivemind working on this kind of thing, I highly encourage you to learn Lean and join this community.