Low-dimensional Lie algebras

Stream: maths

[Paul Schwahn]

Has anyone attempted to formalize classification results for low-dimensional Lie algebras?
I know that the classification of semisimple Lie algebras is an ongoing project, but has anyone worked on other types of Lie algebras?
A few people here at Unicamp are currently trying to tackle this. We have already proved the classification of 2-dimensional Lie algebras (there's just two: the abelian one and the affine one, so far over arbitrary fields). It's not yet mathlib-ready, but we are definitely considering to contribute eventually.

[Oliver Nash]

I don't think anyone has worked on this, I look forward to seeing your contribution when it is ready.

[Oliver Nash]

Note that the semisimple classification is barely being worked on (partly as I got involved in other work). I do hope to return to it at some point next year as a large amount of the theory is in place. If you wish to contribute there, a self-contained piece is #10066 (albeit, not an easy task for a beginner).

[Paul Schwahn]

Thanks for the heads up, that's good to know! When we have something to show, I will post it here.