The Coq mailing list

[Florent Hivert <Florent.Hivert AT lri.fr>]

      Dear Bruno, happy new year,

On Thu, Jan 11, 2018 at 03:39:16PM +0100, Cyril Cohen wrote:
> I am not aware of any Coq development about ((semi-)simple) Lie algebras and
> their classification.

> Unfortunately, I don't know much about semi-simple Lie algebra, so I cannot
> anticipate precisely your needs, but if you are willing to give me more
> details, I could tell you what exists or not in the mathematical components
> library. You can also read the headers of theory files (such as
> mathcomp/algebra/matrix.v, mathcomp/algebra/mxalgebra.v,
> mathcomp/ssreflect/fingraph.v, ...) to check if what notions it covers.

I think I should mention my developement Coq-Combi [1] based on math-comp,
whose main goal was to formally prove the Littlewood-Richardson rule, and the
Frobenius isomorphisms between symmetric functions and the character ring of
symmetric-group. It's maybe not the same corpus of material, but If we believe
the Fulton-Harris book, there are closely related subjects.

It's not clear if you can reuse something from it (maybe partitions), but
conceptually it's not very far. Also I'm close enough to people who
implemented the Root System/Cartan/Coxeter/Lie theory in the computer algebra
system sage and there might probably be design choice which where good on one
side and can be reused.

Anyway, I would be interested to discuss, about such development if not to
help.

By the way, pass my new year wishes to Ilia if you see him !

Best,

Florent

[1] https://github.com/hivert/Coq-Combi