Have any numbers been proven to be normal that weren't constructed to be? It's easy to construct an example of a number that's normal in a given base, but for most given numbers it's notoriously hard to prove that they're normal.
Has any number ever been proven to be normal (either in a particular base or in all bases) that wasn't specifically constructed to be normal? Say, a number that had already been defined and explored in a previous paper not related to normality, but that was only proven to be normal in a later paper. (An answer to this question doesn't need to actually provide the two papers; I'm just explaining what I'm looking for. It doesn't count if the original paper contained an "almost proof" of normality, and then a later paper just filled in a few missing steps.)
The only possible example that I know of are the Chaitin's constants, although I'm not sure whether it was immediately realized that they are normal, or whether it was simple proof once someone thought to ask the question. (Also, Chaitin’s constants are not computable, while I’d prefer an example that’s a computable number.) Ideally, I'd like an example of a highly nontrivial proof of normality for a well-studied number, such that the finding of normality was very "surprising".
I'd also be interested in "nontrivial" proofs of the non-normality of a previously studied number, but I admit that in this case it's hard to pin down exactly what I mean by "nontrivial", because (e.g.) every rational number is not normal.
 A: Quoting from the 2018 Normal numbers and computer science, by V.Becher and O.Carton (In Sequences, groups, and number theory (pp. 233-269). Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-69152-7_7):
"All known examples of normal numbers have been obtained by constructions."
This is not too surprising, if true. This claim is not completely clear (see also the comments below), however it could be somewhat weaker than "have been constructed specifically to show an example of normality". For instance, the Champernowne constant is basic in symbolic dynamics (the expansion of its base-2 version is the model-case of a transitive point, and a recurrent but not uniformly recurrent point, under the shift), and I don't think it was defined by Champernowne in his 1933 paper just, or primarily, to show an example of normal number (but see Timothy Chow's comment below).
This example answers also a question you posed in a comment: normal numbers have important connections with the theory of dynamical systems, among other things. See for instance the 2006 reference work Old and new results on normality, by M.Queffélec.
