The nice thing is, once all of these proofs are formalized in a machine-checkable language, it should be relatively straightforward to translate the corpus between different languages, if someone finds something with a nicer syntax.

If you're doing it for fun anyway, why not use the language that gives you the most pleasure?

Interesting to find this comment, I’ve been dipping my toes into formal methods and was doing a RCoq tutorial yesterday (really basic stuff), and I also noticed that the proofs in RCoq have a more pen -and-paper proof feel to them.

I hear you. :-)

Hearing someone say "the future of proofs is Lean" is a bit like hearing someone say "the future of programming is Rust." Sorry to disappoint, or happy to inform, there are hundreds of programming languages actively being used, and Rust is not even the most used language. To think that proof assistants, fancy programming languages, would be any different is suspiciously motivated.

That's like saying the future of code is Assembler.

Lean is not for humans.