Computer algebra algorithms are basically functions. Axiom is unique in that it organizes the functions based on a group theory scaffold. Thus you can know that certain matrices commute but rectangular ones don't. Algorithms that know how to commute live in the commutative "category" in Axiom. So the game is to distribute LEAN's commutative axioms in their proper place in the group theory inheritance scaffold so they are available when they apply.
Axiom arranges the world into "categories" (not category theory stuff) and "domains". The LEAN structure is a third structure (actually fourth but...) built in parallel so that a theorem that proves that certain matrices commute will only be available when it applies. When you try to prove your algorithm you have a collection of LEAN axioms, definitions, and tactics that are valid and apply to your particular function. If your algorithm used rectangular matrices the commutative theorems would not be visible and thus not available in a proof step. Due to the hierarchical nature, once you prove an algorithm you can also use it in other downstream proofs, for example, using proven data structures and their properties.
I have not published any papers on the subject. I'm no longer anywhere in the academic pipeline so a paper wouldn't get very far. Plus this is "in the cracks" kind of research that doesn't seem to fit into either camp.
As for the education or research question... I'm trying to do what I call "computational mathematics". It would have "real world impact" for Proof Systems so they would be able to depend on and use proven computer algebra results. Computer algebra systems would benefit by giving proven answers. Both areas would benefit.
Don't try to build a computer algebra system from scratch. Axiom has hundreds of years of PhD level research work embedded in its code. There is no way to reproduce some of it as the people have died. Researching just one of the algorithms could take the equivalent of a PhD effort. I tried to introduce literate programming so that people could learn to maintain, modify, and extend Axiom. The idea is that you could "read the docs" and both learn from the authors and have embedded pointers to the theory literature. Without literate programming I believe that the whole effort will eventually die as the learning curve is very steep. Literate programming was an attempt to keep Axiom "alive". Nobody wanted it. I gave a talk on it once: https://www.youtube.com/watch?v=Av0PQDVTP4A&ab_channel=NextD...
There is no "team". There is just me. Apparently I'm bad at "team". I have no desire to get forked again.