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.