> Sadly, everything I understand is most likely already in there, so I doubt I could contribute meaningfully, haha.
I wouldn't be so sure - and even if so then remember there's enormous benefit to improving tooling around a system. If you want to be involved somehow, better devx, tutorials, output, packaging, error messages all make a big difference to end users.
Edit -
As another thought, is there benefit in going through papers and translating that work into lean4? I'm not really familiar enough with it but if so that may
1. Find issues in current work, like Tao did in his own work
2. Add to a reusable body of work
You absolutely can contribute meaningfully
The maths world is incomprehensibly broad and deep, even if you just take the Erdos approach and go for interesting but shallow problems
If you start with nothing (like in the numbers game), simple proofs are a lot of ... just effort, because you have specify a lot of rewrites and overall work. In mathlib, however, systems like simp (the simplification system) or linarith ("There is a solution by linear arithmetic") seem to do a lot of heavy, repetitive lifting by now.
It's a really interesting snowball effect. Sadly, everything I understand is most likely already in there, so I doubt I could contribute meaningfully, haha.