If I could wave my magic wand, I'd have Axiom (or one of its forks) be the "winner" that everybody rallies around, with a change in leadership around it. It has the most advanced math, and it was built by the titans of computer algebra research. To this day, despite being developed by a skeleton crew, it does math no other "more modern" CAS can do. And it's built on a sane language that will never die.
The world deserves a robust, supported, high-performing CAS. Computer algebra could be as ubiquitous to computation as ordinary arithmetic, but everything non-commercial just falls short for general use.
There are some happy accidents like df/dx making sense as both a derivative and a division of 1-forms, but on the whole you can't pick a single notation and hope for it to work well in all situations, yet that seems to be what most algebra systems do out of necessity.
To fix this I reckon we'll need to standardize not the automated algebra part but rather get those systems to communicate using some standardized format. Which is nigh impossible because of the sheer variety of mathematical concepts, but one can hope.
I'm hoping to build a prototype for this sometime in Julia's `Symbolics.jl` CAS. It would be just a simple proof of concept to implement derivative and integral rules from Mathlib or some custom maths library, and get them into the CAS. Symbolics.jl seems to be a perfect fit for this since it's made to be extensible, and Julia's metaprogramming would be a welcome addition as well. Either way, I would love to see this become part of the CAS ecosystem.
Can these efforts be combined into a high quality OS library? The license would permit use from commercial applications like MATLAB. There is precedent in libBLAS.
It looks like lisp... which I have to say is not used much these days.
I feel like at least a large part of the functionality of a general purpose CAS can be written down once, and every CAS out there could benefit from it, similar to what the Language Server Protocol did for programming tools. They also had to rewrite the same tool for some language multiple times because there are lots of editors out there, and the LSP cut the time investment down a lot. They did have to invest a large amount of time to get LSP up and running, and it'll have to be maintained, but I think it's orders of magnitudes more efficient than having every tool developed and maintained for every single (programming language, editor) pair out there.
Main problem is like you said how to write down mathematical knowledge in a way that all CASs can understand it. I've been learning about Mathlib lately [0], which seems like a great starting point for this. It is as far as I know one of the first machine readable libraries of mathematical knowledge; it has a large community which has been pushing it continuously forward for years into research-level mathematics and covering the entire undergraduate maths curriculum and it's still accelerating. If some kind of protocol can be designed to read from libraries like this and turn it into CAS code, that would be a major step towards making the CAS ecosystem more sustainable I think.
It's not exactly what you were talking about, as in, this would allow multiple CASs to co-exist and benefit from each other, but I think that's better than having one massive CAS that has a monopoly. No software is perfect, but having a diverse set of choices that are open source would be more than enough to satisfy everyone.
(I have posted about this before [1] on the Lean Zulip forum. It's open to everyone to read without an account)
[0] https://leanprover-community.github.io/ [1] https://leanprover.zulipchat.com/#narrow/stream/113488-gener...
