Hello,
(1) I have been trying to organize a list of project ideas for people who want to learn Mizar (but don't know where to begin, or need some additional "push" to get started):
https://thmprover.wordpress.com/projects/
(2) I have a few more projects in the pipeline, but I don't want to encourage people to work at cross purposes...especially with people who are already working on these things! (Since Loops are rather niche, especially Symplectic 2-Loops, I figured I was safe; the Octonions might be running into trouble duplicating someone else's work-in-progress.)
The projects I have in mind are oriented towards formalizing the notion of the tensor algebra of a module in Mizar. But I wanted to bring it up here to avoid "collisions".
Therefore, is anyone working on anything related to the tensor product of modules (or the tensor product of Abelian groups)? I want to avoid undermining your efforts, or duplicating your work.
Best,
Alex