specific-question Is the tag formal-proof used correctly in the questions Convergent sequences in projective varieties? Here on MO the tag has empty tag-info, but if it was created with similar intentions as on Math.SE, it should be used for profs with various formal systems.

This is what the tag-info on Mathematics says:

> For questions about proofs within a formal system, such as natural deduction or a Hilbert system.

If the intended usage of this tag is similar as on Mathematics, it might be worth adding it to the list of tags which are often used incorrectly: chat.stackexchange.com/transcript/10243/2018/9/1

Of course, the fact that the (proofs) tag was removed might have as a consequence that people might try to use some other tag containing the words "proof" if they are asking for a proof (or about a proof) of something.

@MartinSleziak I agree with the suggestion that a lot of people don't know what formal proof means, and it should be flagged as such. It does indeed mean a proof in the strictest possible sense, possibly even more strict than the Mathematics definition, say for only those proofs dome in a proof assistant.

The tag (formal-proofs) have been removed in that question by David Roberts.

BTW today some user tried to ping you in the main chat room - it seems to be something related to a question on hsm.

But I guess you noticed. (If you look in here, it's quite likely that you looked also into the main chatroom.)

I'm not sure to which extent it is really relevant for you - it seems that they quote you in a comment, but it's unclear where the comment is taken from.