Collaboration for formalization of Lie Algebras

--0000000000001f45930656495941
Content-Type: text/plain; charset="UTF-8"

Hello there,

Alex Nelson and I are currently working on the formalization of the
classification of simple Lie Algebras. We are making good progress, but it
is just *so much* to formalize. Hence we are looking for collaborators to
speed up the process.

We are happy for any researcher wanting to join, but this might be a chance
especially for your students who are interested in Mizar. We can whip up
abstracts with skeleton proofs quickly. For example, an article whose
proofs I want to delegate is our candidate for RING_6, which shall be about
the the product and sum of a family of rings. It will be pretty close to
the existing proofs in GROUP_7 and I'm already doing the product and sum of
Algebras, which is very similar.

We offer abstracts, authorship, guidance and emotional support. We have no
funding though. If you like Algebras (or even if you don't, like me) and
have the free time, you should join! The main communication platform will
be Discord. If you are interested, please send me your Discord handle via
[email protected]


Best regards and stay healthy
Sebastian Koch

--0000000000001f45930656495941
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">Hello there,<div><br></div><div>Alex Nelson and I are curr=
ently working on the formalization of the classification of simple Lie Alge=
bras. We are making good progress, but it is just *so much* to formalize. H=
ence we are looking for collaborators to speed up the process.</div><div><b=
r></div><div>We are happy for any researcher wanting to join, but this migh=
t be a chance especially for your students who are interested in Mizar. We =
can whip up abstracts with skeleton proofs quickly. For example, an article=
 whose proofs I want to delegate is our candidate for RING_6, which shall b=
e about the the product and sum of a family of rings. It will be pretty clo=
se to the existing proofs in GROUP_7 and I&#39;m already doing the product =
and sum of Algebras, which is very similar.</div><div><br></div><div>We off=
er abstracts, authorship, guidance and emotional support. We have no fundin=
g though. If you like Algebras (or even if you don&#39;t, like me) and have=
 the free time, you should join! The main communication platform will be Di=
scord. If you are interested, please send me your Discord handle via <a hre=
f=3D"mailto:[email protected]">[email protected]</a></div=
><div><br></div><div><br></div><div>Best regards and stay healthy</div><div=
>Sebastian Koch</div></div>

--0000000000001f45930656495941--