That's very interesting, I'm no mathematician but I should have a play around with it.

> 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