5 of 9 replaced http://meta.math.stackexchange.com/ with https://math.meta.stackexchange.com/

What's the (formal-proofs) tag for?

The tag currently has no tag wiki. In my opinion this might invite people to use the tag for any question asking for a (more or less formal) proof. Very similar to the way the tag was used before it got removed and blacklisted. My personal assumption, however, was that is more likely intended for questions on a way more formal level, where you are considering a strict formalism and how to perform low-level steps in a formal proof.

Currently, has 26 questions, half of them from this month. Several older questions are indeed related to formal questions, while recent examples are at a much less formal level.

  1. Do you agree that is not intended for any question where a proof is required, but only for questions where the formalization plays a major part?
  2. How does the tag differ from ? Is it that is intended for questions about a specific proof, while is on the meta level, speaking about (a family of) proofs?
  3. Do you have a specific wording to suggest for the tag wiki?