The Coq mailing list

[Cyril Cohen <cohen AT crans.org>]

Dear Bruno, happy new year,

I am not aware of any Coq development about ((semi-)simple) Lie algebras 
and their classification.

However, the mathematical components library 
(https://github.com/math-comp/math-comp) has integers, matrices (and a 
lot of linear algebra in finite dimension) and finite graph theory 
(there is no specific theory for trees, but you could develop it 
yourself as a subtype of finite graphs).

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.

Best wishes,

--
Cyril Cohen


On 01/01/2018 22:18, Bruno Le Floch wrote:
> Hello, and happy new year,
>
> Has the classification of (semi-)simple Lie algebras [1] and their root
> systems been formalized in Coq?
>
> Googling only gave the page "Formalizing 100 Theorems" [2], which lists
> this among problems it does not track.  Are there current efforts in
> this direction?  The classification boils down to a combinatorial
> question about matrices of integers, then to a classification of certain
> graphs and trees.  Where can I learn of existing libraries to manipulate
> such objects?
>
> Unimportant background: to prove some property of representations of
> simple Lie algebras, we had to perform a somewhat tedious case by case
> analysis (doable by hand), which we have started formalizing in Coq [3].
>   For now we are using the classification of simple Lie algebras (and
> their weights and roots) as a black box since it is well established.
> However, that increases chances of typos or bugs in the code listing
> various conditions on weights of each Lie algebra.
>
> Thanks in advance for any information,
>
> Best regards,
>
> Bruno
>
>
> [1]:https://en.wikipedia.org/wiki/Semisimple_Lie_algebra
> [2]:http://www.cs.ru.nl/~freek/100/
> [3]:https://github.com/blefloch/lie-algebra-w0
>    (Admittedly the code is ugly: I started learning Coq a month ago.)