I want to synthesize and organize prior discussions into a research statement.
Scratchpad was born as a research platform. Axiom is the commercial
version that was forcibly birthed due to IBM's business decisions. Axiom
has never been, and was not intended to be, a "commercial competitor
to Mathematica and Maple".
If your goal in developing a new algorithm is to have people use it
then it makes more sense to write it in Mathematica and Maple.
If your goal is to research an extension of existing theory, write it in Axiom.
Completing the Risch algorithm would be a perfect Axiom-style goal.
There are 3 interesting streams of research that are currently active and
of interest to Axiom. These are computer algebra, proof theory, and type theory.
All three have been active since the last century. The interesting research
question is "What does this have to do with Axiom research?"
Computer Algebra stream
Axiom differs from other computer algebra systems because it has a
scaffold of group theory guiding the structure. This has defined the whole
category / domain organization.
Because of the group theory structure, Axiom is an ideal platform for
organizing and optimizing algorithms within the web of existing ideas.
One research question is the impact of dependent types on the potential
for re-organizing the Axiom structure. Another question is how to adapt
Lean proofs to proving Axiom's algorithms.
Proof theory stream
Lean is the latest version of decades-long research in proof assistants.
It is effectively a from-scratch implementation of the ideas, implemented
within a programming language that will self-host.
Lean has inspired a large body of proofs ranging from undergraduate to
leading edge research.
Lean contains proofs related to group theory, thus making it a compatible
match to Axiom. A second scaffold that contains the definitions and theorems
along side Axiom's group theory structure would make it possible to inherit
the definitions and theorems when trying to prove Axiom algorithms.
In addition, since Lean is pushing into areas of proof that could usefully be
implemented in Axiom, it opens a stream of new areas of algorithms. An
exciting version of this would be automatic generation of algorithms from proofs.
Type Theory stream
Type theory has the notion of a "dependent type". This allows a type to be
specialized based on the arguments of the type. Axiom would take "types"
beyond the programming language domain and into mathematics.
Axiom does this in rather limited ways at the moment. For example, there
is the general GCD algorithm. Axiom contains about 20 implementations based
on the place in the type hierarchy they reside.
Using dependent types, the GCD algorithm could be written once
and specialized as needed. Further, the proof of the algorithm is not really
dependent on the proof of the instance if done properly. This has the potential
of collapsing the many existing Axiom specializations, such as packages, into a
single instance.
Peak wave, Peak trough
The Axiom research platform sits where these three waves come together.
The Lean proof of the GCD in a dependent type implementation restructures
the Axiom algorithm hierarchy. The goal is proven algorithms in a general setting
that specialize for a given algorithm.
Such a "computational mathematics" platform would bring together disparate
existing streams. That's the goal of the SANE (rational, coherent, judicial, sound)
branch of Axiom research.