It consists of an interpreter environment, a compiler and a library, which defines a strongly typed hierarchy.
The first one was started in 1965 by James Griesmer[2] at the request of Ralph Gomory, and written in Fortran.
Early consultants on the project were David Barton (University of California, Berkeley) and James W. Thatcher (IBM Research).
The current research direction is "Proving Axiom Sane", that is, logical, rational, judicious, and sound.
The primary philosophy is that Axiom needs to develop several fundamental features in order to be useful to the next generation of computational mathematicians.
Axiom plans to use proof technology to prove the correctness of the algorithms (such as Coq and ACL2).
The latest image is available on any platform using docker and the commands: In Axiom, each object has a type.
Axiom has an implementation of the Risch algorithm for elementary integration, which was done by Manuel Bronstein and Barry Trager.
While this implementation can find most elementary antiderivatives and whether they exist, it does have some non-implemented branches, and raises an error when such cases are encountered during integration.