I am interested in contributing to the formalization of mathematics, but I don't know the extent to which such activities are publishable. Here are some questions in this vein:
How can one determine whether a piece of formalized mathematics is publishable? If the math is new, then it's publishable even without formalization. If the math is old, but the formalization is new, then I assume it is publishable. What if a piece of mathematics has already been formalized in language X, but you are the first to formalize it in language Y?
What are the appropriate venues to publish formalized mathematics? I assume there is a hierarchy of outlets, but I'm not familiar with them.
What are the best practices for publishing formalized mathematics that make use of libraries that change over time? For example, if one writes a proof in Lean, must the contribution be included in
mathlibbefore submitting for publication somewhere?