Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Do you actually need canonization, or would a complete invariant suffice for your purposes? Although the two are computationally equivalent for graph isomorphism (there is a polynomial-time canonical labelling algorithm for graphs iff there is a poly-time complete invariant), this seems not to be true in general. So a complete invariant might be easier to find.
If a Lie algebra is given to you not as matrices but just by generators and relations, then first translating it into matrices may be prohibitively expensive. The current best upper bounds on the faithful representation you get from Ado's Theorem are horrible from the complexity perspective (I believe it's something like $n^c$ for Lie algebras of nilpotency class $c$ - since the nilpotency class can be as large as $n-1$ in general, this is pretty huge).
François: Thanks! Not being a logician, I didn't know about the Lindenbaum-Tarski algebra. But if I've understood correctly, atoms in the Lindenbaum-Tarski algebra of $T$ (if any exist) are exactly the minimally unprovable statements over $T$.
@Matt Brin: I know :(. The issue with the way you've phrased it (which I thought about) is that by definition nothing strictly weaker than $S$ can prove $S$, because "$R$ is strictly weaker than $S$" means that $S$ implies $R$ but not vice versa. Minimally unprovable statements are statements that entail no consequences other than themselves. So the question doesn't quite capture my original motivation, but nonetheless that was my original motivation. (And for the original motivation, the answer is trivial.)
