Equal signs with fancy marks Some people use $\stackrel{\mathrm{def}}{=}$, $:=$ or $\stackrel{\Delta}{=}$ for definitions.
In more informal contexts, I have also seen $\stackrel{?}{=}$, for "I wish to prove this equality, which implies the thesis", used when working backwards, or even the less common $\stackrel{!}{=}$ (for which it is difficult to infer a precise meaning, but it's something like "we are imposing this equality", or "this is an Ansatz").
It seems like the use of these symbols is not common in papers (apart from maybe the first ones for definitions); however, they seem useful to me as a way to convey more meaning than the usual equality symbols. For instance, in some sense the "?" superscript changes the set of "allowed operations": from $a=c$ and $b=d$ it follows that $a+b=c+d$, but the same implications wouldn't hold with $\stackrel{?}{=}$ signs.
Q1: has the use of these symbols ever been properly formalized?
Q2: are there contexts in which they are used in papers? Are they standard in your field? Are they used in lectures/seminars/papers?
 A: In a slightly different direction, $\overset{\mbox{(2.3)}}{\ge}$ (the overset should be in a smaller font using \tiny, but for some reason that wouldn't render here) is a nice way to indicate that the inequality uses $(2.3)$ - this is especially convenient with a long string of inequalities in display-math where it's otherwise hard work to figure out which inequality uses which previous calculation.
A: One context in which the distinction between "equal by definition" and "equal because we proved it" has a precise mathematical meaning is intensional dependent type theory.  This includes formalizing mathematics in a computer proof assistant based on ITT, such as Coq or Agda, but mathematics in ITT can also be done "unformalized" such as in the homotopy type theory book.
As for notation:


*

*Coq uses $=$ for propositional equality (i.e. "we proved it" equality) and $:=$ for definitional equality (more precisely, for definitions currently being made).

*Agda uses $=$ for definitions being made, and (at least in the standard library) $\equiv$ for propositional equality.

*The HoTT book uses $=$ for propositional equality, $\equiv$ for an equality that holds by definition but is not something currently being defined, and $:\equiv$ for something currently being defined.
We spent a long time deciding on this; we wanted to use $=$ for "ordinary" equality, and we wanted to use something symmetric like $\equiv$ for equalities-by-previous-definition and something asymmetric like $:=$ for current-definitions so as to indicate visually that the left side is what's being defined.  But $:=$ for a current-definition would suggest that it's a propositional equality that results rather than a definitional one, which led us to invent the symbol $:\equiv$.  (We then actually ended up using $:=$ later for a "propositional equality being currently defined to hold", which happens under some versions of higher inductive types.)
