4:38 PM
Is the tag 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.
0

It's very well known that if $X$ is an irreducible projective variety (feel free to assume that the base-field is $\mathbb{C}$), then any two points $x,y\in X$ can be connected by the image of a non-singular curve. An outline of the proof can be found here. Anyway, the stardard reference for the ...

4:50 PM
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

1 hour later…
6:12 PM
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.

4 hours later…
9:49 PM
@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.

1 hour later…
11:15 PM
The tag (formal-proofs) have been removed in that question by David Roberts.
@DavidRoberts Thanks for your edit.
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.