How are formal definitions in mathematics created/discovered? We are talking about the formal definitions. How do mathematicians decide what the formal definitions should be like in the first place and what does the process look like when they refine it?
 A: The process is individual. A mathematician would define something if it is convenient to do so. If that concept proves useful, and catches on, the definition will be used by others. Along the way people might adjust the definition, according to need. It's a completely free process, without any rules or governing bodies. 
A: Definitions often come along with mathematics naturally. For Lie algebras, say, many definitions have been made following the example of groups, which were studied a long time before Lie algebras.
Examples of such definitions are "solvable Lie algebras", "nilpotent Lie algebras", "simple Lie algebras", "radical of a Lie algebra" etc.
The motivation, among other things, was to classify
certain classes of Lie algebras, e.g., the complex simple finite-dimensional Lie algebras. For the structure theory of semisimple Lie algebras many new definitions were made, and they were very natural (e.g., "root spaces", "Dynkin Diagrams", "Cartan matrices", "Killing form" etc.).
A: People like to think that mathematics, being very theoretical and abstract, is different from other natural sciences.
And in a way, it is, because there are different criteria for proofs and the lack of paradigm shifts (or at least the lack of paradigm shattering) do cause mathematics to be slower to progress, and much more sturdy against changes when compared with physics or chemistry.

However, ultimately the research itself is not very different from any other research. Let me share my experience, as in my Ph.D. I had to come up with a new kind of definition. Specifically for something called "iteration of symmetric extensions".
You start with an example, and you ask yourself "How can I make this specific example work?" and you try to figure out which properties are due to the example being specific, and which properties can be generalized.
So you write a definition, and you try to prove theorems that you think should hold for your construction. Then you get stuck, and you take a closer look at the example, and you realize that you miscalculated something, so you change the definition, and you change the theorems.
But you keep coming back to the example. And once you nailed that one, you move to another example, perhaps somewhat with a different nature or a different level of complexity. And you throw that specific example against your definitions and theorems, and you check if everything works out.
Of course it doesn't work out. So you need to modify the definitions in a way that would reconcile the first example's nature with the second example. And so you continue with a few examples, until you manage to get something which you think is right.
Later on, if you're lucky enough, other mathematicians will take interest in your work and your definitions. They will work through them, and see problems or ideas how to simplify them. They might be interested in some specific family of cases, which will then get an adjective like "normal" or "regular" in some cases, or just a specific term designed to separate the "interesting and relatively simple cases" from the "difficult cases".
And this is the story of formal definitions. They start from an idea, and a few toy samples. Then distilled into general and abstract definitions, which later gets changed as they are adopted to a workable framework by the mathematical community.
