The [tag:formal-proofs] 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:proof] tag was used before [it got removed and blacklisted](https://math.meta.stackexchange.com/a/2126). My personal assumption, however, was that [tag:formal-proofs] 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, [tag:formal-proofs] has 26 questions, half of them from this month. [Several](https://math.stackexchange.com/q/931681) [older](https://math.stackexchange.com/q/961994) [questions](https://math.stackexchange.com/q/939261) are indeed related to formal questions, while [recent](https://math.stackexchange.com/q/962636) [examples](https://math.stackexchange.com/q/962712) are at a much less formal level. 1. Do you agree that [tag:formal-proofs] 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 [tag:proof-theory]? Is it that [tag:formal-proofs] is intended for questions about a *specific* proof, while [tag:proof-theory] is on the meta level, speaking *about* (a family of) proofs? 3. Do you have a specific wording to suggest for the tag wiki?