The [tag:formal-proof] 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](http://meta.math.stackexchange.com/a/2126). My personal assumption, however, was that [tag:formal-proof] 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-proof] has 26 questions, half of them from this month. [Several](http://math.stackexchange.com/q/931681) [older](http://math.stackexchange.com/q/961994) [questions](http://math.stackexchange.com/q/939261) are indeed related to formal questions, while [recent](http://math.stackexchange.com/q/962636) [examples](http://math.stackexchange.com/q/962712) are at a much less formal level. 1. Do you agree that [tag:formal-proof] 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-proof] 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?