The Coq mailing list

[Bruno Le Floch <blflatex AT gmail.com>]

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.)