Axiom is alive, well, and under active development. The current effort is merging the
LEAN [0] proof technology with the Axiom algebra. This involves some deep restructuring.
The target result is proven algorithms, something missing in current CAS work.
The effort involves building a parallel architecture to the current Axiom
category / domain layout to enable functions to use LEAN's axioms, definitions,
and tactics to prove existing algorithms.
In addition, Axiom now uses Common Lisp CLOS to enable work using dependent
types, something not currently available in the legacy system. The algebra
hierarchy is now a CLOS hierarchy which enables a lot of flexible extensions.
There is no point in publishing the work as open source since it is still
in the active research phase. When released it will be announced on the
http://axiom-developer.org website and uploaded to github.
One of the Axiom algorithms (Groebner basis[1]) has been proven in Coq.
Wikipedia contains the literate form of Axiom[2] , including the original book
restored from the NAG files.
There is an active fork maintaining the legacy code as mentioned above.
[1] Bruno Buchberger. Bruno buchberger’s phd thesis 1965: An algorithm for
finding the basis elements of the residue class ring of a zero dimensional
polynomial ideal. Journal of Symbolic ComputationVolume 41,
Issues 3-4, Logic, Mathematics and Computer Science:
Interactions in honor of Bruno Buchberger (60th birthday),, 2006.
So first of all thank you Axiom and all the work you have put in the system over the years. Second, the integration with LEAN seems like an amazing step forward. Is there anything on the internet I can read more about this? How would it work? Would it be beneficial for education purposes or mainly for research?
Third, I am otherwise engaged in other projects these days, but a long life dream of mine is to build a CAS from scratch. That said, I wouldn't mind start collaborating with a team improving an existing one like Axiom. The "How to participate" link is just "TODO", is there any way I can get in touch with the development team?
Thanks for the "all the work" complement. Despite all, it is more fun than work.
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.
Having experience with prior open source work I'm not likely to release
the current effort until I'm much closer to completion. The whole idea
of CAS and Proof has already generated a hostile reception from both areas
in my email stream.
I've already proven that if I did release Axiom again I'm too socially inept to
manage the process anyway. I'd release a technical paper or two but I'm
no longer associated with CMU so I'm pretty much a "hobby researcher" I guess.
The last Axiom presentation was the invited talk at Notre Dame prior to Covid.
There are a lot of interesting things "in the works" though. One is the
idea of "proof down to the metal" (aka Proof Carrying Code[0]). The use of (FPGA)
field programmable gate arrays[1] and the RISC-V[2] architecture soft-implemented
in the FPGA means that I can run the LEAN proof in parallel with the algorithm at
the hardware level. This not only proves the algorithm correct, it proves the
implementation correct. I have a few FPGAs.
It's all fun and games but I have to wait to release it.
"Faszinating" that a lot of these systems seem to be implemented from scratch in object-oriented C++ (?), instead of Prolog, SML, OCAML, Haskell, Lisp, ... what went wrong?
Scratchpad lives on in FriCAS https://github.com/fricas/fricas/commits/master/ which has commits 18 hours ago. Tim Daly worked diligently on Axiom for years. However some of his changes, like requiring every single file be literate code and complete refusal to compromise, turned decades of IBM research into an isolated dumpster fire; good luck getting it to build/run anywhere outside his Docker container. I'm reasonably happy with FriCAS since it's based on the same software and is much more open source normative, while possessing capabilities Maxima users could only dream of. See also https://lists.nongnu.org/archive/html/axiom-developer/2007-0... and https://lists.nongnu.org/archive/html/axiom-developer/2007-0... for evidence of his leadership style.
I use Maxima regularly as it was what I was taught at university. It is updated regularly. It's cranky as hell but it works. Sometimes I use the CAS on my calculator, mostly to check my own work, because it hurts less. That's an HP Prime with Giac/Xcas on it.
I like the idea of learning to use Axiom, but getting it to run has been a huge PITA, at least on PopOS using the distro packaged version. In fact, I never did get that to run. So I switched to using Tim's Docker image and even that failed at first:
$> docker run -i -t daly/axiom axiom
yields
personality change failure 1
But after a bit of digging, I finally found the solution for that. It's related to a seccomp setting, which can be toggled with a command lines switch.
So this will yield a running Axiom instance:
$> docker run --security-opt seccomp=unconfined -i -t daly/axiom axiom
As a side note to all of that... when I first decided to take a stab at getting a CAS running on my laptop, I tried all of Maxima, Axiom, FriCAS, and, uh, probably some others I'm forgetting. And NONE of the distro packaged versions worked out of the box. All would fail on startup with some variation of:
The assertion realpath(s,o) on line 471 of main.c in function mbin failed: Invalid argument
or
** buffer overflow detected *: terminated
I finally got Maxima working somehow, and that's been my goto CAS ever since, just because it worked. Weird, but it is what it is.
I worked on/with CAS in the 1990s, mostly PARI/GP (as a researcher) and Maple (as an assistant/junior professor).
I remember watching a talk by one of the Axiom developers, maybe T. Daly himself, on the Jussieu University Campus in Paris, probably around 1998 or 1999. I remember being impressed by some of the ideas that were presented (I may even have asked 1 or 2 silly questions during the seminar), but unfortunately the system was not yet open source and so this was of little use for me.
There were quite a few challenges before Axiom could be open sourced.
NAG released the Axiom sources to me around that time. I gave an
invited talk in Paris.
There were many issues to solve. The primary one was that you needed
a running Axiom to build Axiom. I was not allowed to distribute the
NAG version of a running Axiom. It took a long time to restructure the
system so it could be built from sources.
Portions of the NAG version were never distributed to me and I had
to recreate some from scratch.
GNU hosting and Sourceforge hosting were new technologies I had to master.
I also struggled to understand how to create and lead an open source effort.
Obviously in hindsight I'm very bad at management.
The NAG version of the system removed the Common Lisp version of AKCL,
(of which I'm a minor author). AKCL is now GNU GCL under Camm.
IBM Research sponsored the creation of AKCL under contract
which was developed by Bill Schelter. Bill and I were in constant
contact and he used my office on his site visits. I had to re-host
Axiom on AKCL from the NAG version but Bill was dead by then.
Back then I was working at City College of New York in the CAISS effort
involving Infinite Group Theory (Magnus). I maintained, modified, and extended
that effort and made it open source. Axiom was not part of my job
effort until the last few months of my time there. Axiom was all
after-hours / off-the-clock work. (I see my name has been "scrubbed"
from the CAISS/Magnus work. They even mention Axiom but not me. Sigh.)
Axiom is now exploring new research ideas combining computer algebra
and proof theory (aka computational mathematics). The computer algebra
people don't do proofs and the proof people don't do computer algebra
algorithms. In fact, of the few hundred papers I reviewed only James
Davenport made the bibliography section in both areas. I'm not expecting
any enthusiasm for this research. If I fail no one will notice. If I
succeed ... no one will notice :-) But I'm having fun.
> For example, Axiom's integrator gives you the answer when an answer exists. If one does not, it provides a proof that there is no answer. Integration is just one of a multitude of symbolic operations that Axiom provides.
What does "an answer exists" in this case? Is axiom able to prove that an integral does not have an answer mathematically, which seems impressive, or just that it can not be found using its own substitucion rules?
Axiom is alive, well, and under active development. The current effort is merging the LEAN [0] proof technology with the Axiom algebra. This involves some deep restructuring. The target result is proven algorithms, something missing in current CAS work.
(Note that this is project goal F on http://axiom-developer.org)
The effort involves building a parallel architecture to the current Axiom category / domain layout to enable functions to use LEAN's axioms, definitions, and tactics to prove existing algorithms.
In addition, Axiom now uses Common Lisp CLOS to enable work using dependent types, something not currently available in the legacy system. The algebra hierarchy is now a CLOS hierarchy which enables a lot of flexible extensions.
There is no point in publishing the work as open source since it is still in the active research phase. When released it will be announced on the http://axiom-developer.org website and uploaded to github.
One of the Axiom algorithms (Groebner basis[1]) has been proven in Coq.
Wikipedia contains the literate form of Axiom[2] , including the original book restored from the NAG files.
There is an active fork maintaining the legacy code as mentioned above.
[0] The LEAN Theorem Prover https://www.andrew.cmu.edu/user/avigad/Papers/lean_system.pd...
[1] Bruno Buchberger. Bruno buchberger’s phd thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Journal of Symbolic ComputationVolume 41, Issues 3-4, Logic, Mathematics and Computer Science: Interactions in honor of Bruno Buchberger (60th birthday),, 2006.
[2] Wikipedia Axiom https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system...