The problem is that the administration of the university needs an easy metric to decide promotions. So we are stuck to paper count. It's too easy to game, add citations. Now add journal impact index, quartiles, h-index and whatever is the new fad.

How does your idea provide a nice metric if the submissions are anonymous?

Or in other words, who is going to pay us for this?

Unfortunately attaching a corporation name to a statement is a large part of the motivation for a company to spend millions on tokens for Lean proofs. It's a marketing/PR spend for them. Without their name attached, the return on investment is far less.

That said there are some efforts in the direction you're suggesting. For example

- [Prove2Me](https://beta.prove2.me) - Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. One creates open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

- [Tau Ceti](https://github.com/TauCetiProject/TauCeti) - An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics