 harmonic.fun

They seem to do autoformalization, automated theorem proving and code generation, and they use Lean a lot. Sounds fun.