There is a correspondence between Lie algebras and groups on the level of their "algebra", in that many "purely algebraic" theorems in group theory correspond exactly to "purely algebraic" theorems in Lie algebras, and one can often see the exact form of the translation, pretend your group $G$ was a Lie group, and take the Lie functor.
Some examples of this are the definitions and properties of solvability/nilpotence, simplicity, semidirect products, etc.
This also manifests in the fact that the category of group representations for any group has way more structure than might be naively expected, coming from Hopf algebra structure of $k[G]$. We also have this for Lie algebras, coming from the Hopf algebra structure of $U_\mathfrak{g}$, and morally, this hopf algebra structure is the "linearised" version of the Hopf algebra structure on groups.
What is the correct formal way to view the similarity between these theories? Is there a precise formulation of this translation principle, in terms of the (first order?) theories of the axioms of groups/lie algebras?