Hi there! I wanted to ask if it would be okay to create a [mizar] tag (see). Currently I feel like I'm pretty much the only SE user who would use this (apart from random Encounters, see), but I would like to add some FAQ-style question/answers to SE, since the Mizar doc is kinda sparse

I would definitely use theorem-provers for such questions. Notice that the tag-info explicitly mentions Mizar and some other theorem provers.

Whether or not to create a separate tag in addition to this general tag is another question.

@MartinSleziak Thanks for the tag info, I wasn't Aware of that. I think it's fine. Maybe in a few years, when Mizar becomes (hopefully) more popular, an own tag would make sense, but since it's explicitly mentioned, that'll do, thanks.

That reminds me: How much rep until I can simply Change tags without editing the question?

there seem to be some wrongly tagged questions in that category

There is a separate tag for coq on MO: mathoverflow.net/questions/tagged/coq I do not see a tag for specific theorem prover on this site.

There are these two questions which are specifically about Mizar: Importing (translating) Mizar into Coq (Axiomatic set theory into constructive type theory) and Is the Mizar System feasible for checking basic proofs?

@SK19 I am not strongly against to the idea of the new tag. But it should be only added for questions specifically about Mizar (not to question where it is only mentioned in passing). And I would suggest to use it always together with the more general tag.

By which I mean theorem-provers.

To explain what I mean - if there is a question about NBG and it mentions that it is used by Mizar, it probably does not deserve the tag. If the question specifically asks what are the implications of the fact that Mizar uses NBG for the results you get, then mizar would be an appropriate tag.

Does it use NBG or something else? (I have forgotten since I've looked into this.)

@SK19 My personal opinion is that the best solution would be to ask on meta - either in a separate question or in the Tag management thread - to see what other users think about the new mizar tag. And create the tag only if there is some support on meta.

Here is a conversation about coq tag on MathOverflow. Although nothing much is said there - but at least it is clear from that conversation that the tag is not used that much, although it exists and there are Coq-related questions.

@SK19 I am not sure whether you are asking about inline tag-edits - which come at 10k. Or whether you are asking about retagging without bumping - which is not possible.

It is true that many people use theorem-provers tag for basically anything related to some proof. Which is why we have a comment template for this tag. And maybe this tag could also have a tag-warning.

WP: Mizar system

> The MML is built on the axioms of the Tarski–Grothendieck set theory.

I remembered that it is something different from ZFC, but I did not remember which axiomatic system exactly is used there.