Projects in Mizar

--0000000000007067790629b5f67f
Content-Type: text/plain; charset="UTF-8"

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

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

<div dir=3D"ltr">Hello,<br><br>(1) I have been trying to organize a list of=
 project ideas for people who want to learn Mizar (but don&#39;t know where=
 to begin, or need some additional &quot;push&quot; to get started):=C2=A0<=
a href=3D"https://thmprover.wordpress.com/projects/">https://thmprover.word=
press.com/projects/</a><div><br></div><div>(2) I have a few more projects i=
n the pipeline, but I don&#39;t want to encourage people to work at cross p=
urposes...especially with people who are already working on these things! (=
Since Loops are rather niche, especially Symplectic 2-Loops, I figured I wa=
s safe; the Octonions might be running into trouble duplicating someone els=
e&#39;s work-in-progress.)</div><div><br></div><div>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 &quot;collision=
s&quot;.</div><div><br></div><div>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=
.<br><br>Best,<br>Alex</div></div>

--0000000000007067790629b5f67f--