Mathematics Software Projects

There are many software projects which allow us to model mathematics such as:

These types of programs have different purposes but they also have many similarities, I have discussed an example of each of these types of program below:

Each of these programs uses its own computer language to code information about mathematical structures. I think this makes sense since no program can represent all of mathematics, it is effectively infinite, so we cant include all mathematical sructures with the program. All we can do is to provide some common structures and then let users add their own structures using a language designed for this.

Lets look at how these programs represent mathematical structures using their own languages.

FriCAS (an example of a CAS)

FriCAS is an example of a computer algebra system (CAS) . FriCAS is a fork of the Axiom project, more about FriCAS here. FriCAS allows mathematical structures to be specified in a language called SPAD like this:

)abbrev category ABELMON AbelianMonoid
++ Author:
++ Date Created:
++ Date Last Updated:
++ Basic Functions:
++ Related Constructors:
++ Also See:
++ AMS Classifications:
++ Keywords:
++ References:
++ Description:
++ The class of multiplicative monoids, i.e. semigroups with an
++ additive identity element.
++ Axioms:
++   \spad{leftIdentity("+":(%,%)->%,0)}\tab{30}\spad{ 0+x=x }
++   \spad{rightIdentity("+":(%,%)->%,0)}\tab{30}\spad{ x+0=x }
-- following domain must be compiled with subsumption disabled
-- define SourceLevelSubset to be EQUAL
AbelianMonoid() : Category == AbelianSemiGroup with
      0 : constant -> %
        ++ 0 is the additive identity element.
      sample : constant -> %
        ++ sample yields a value of type %
      zero? : % -> Boolean
        ++ zero?(x) tests if x is equal to 0.
      "*": (NonNegativeInteger,%) -> %
        ++ n * x is left-multiplication by a non negative integer
      import RepeatedDoubling(%)
      zero? x == x = 0
      n : PositiveInteger * x : % == (n::NonNegativeInteger) * x
      sample() == 0
      if not (% has Ring) then
          n : NonNegativeInteger * x : % ==
              zero? n => 0
              double(qcoerce(n)@PositiveInteger, x)


The above code is specifying a 'category' this is effectively a set of function signatures like an 'interface' in other languages. We can then implement instances of that, called 'domains', which effectively implement algorithms to construct instances. In these respects FriCAS is very similar to mainstream computer languages, however FriCAS has many powerful capabilities that mainstream languages don't (discussed on these pages). The point I would like to make here is that the axioms for this structure are given in comments only and can't be used to influence instances of this structure or even to check code.

CASL (an example of an Algebraic Specification Language)

CASL is an algebraic specification language, its purpose is completely different to FriCAS, it is used as a means to specify more general computer programs. There is some information about CASL in its reference manual and its libraries in section 'v'. However, like FriCAS it does have its own language (and library of code) that can be used to specify mathematical structures.

spec Monoid =
     sort Elem
     ops  e:       Elem;
          __ * __: Elem * Elem -> Elem, assoc, unit e

spec CommutativeMonoid =
     op __ * __: Elem * Elem -> Elem, comm

spec Group =
     forall x: Elem
     . exists x': Elem . x' * x = e   %(inv_Group)%

spec AbelianGroup =

spec Ring =
     AbelianGroup with sort Elem,
                       ops __ * __ |-> __ + __,
                           e       |-> 0
     Monoid with ops e, __*__
     forall x,y,z:Elem
     . (x + y) * z = (x * z) + (y * z)          %(distr1_Ring)%
     . z * ( x + y ) = (z * x) + (z * y)        %(distr2_Ring)%

view AbelianGroup_in_Ring_add:
     AbelianGroup to Ring =
     ops e |-> 0,
         __ * __ |-> __ + __

The interesting thing for me, about this language, is that it encodes both the function signatures and the axioms. Common axioms are represented by 'assoc', 'unit e' and 'comm' but any other axiom can be specified by using equations and quantifiers.

Isabelle (an example of a Proof Assistant)

Again, Isabelle has a completely different purpose and again it has its own language (and library of code). Isabelle is a proof assistant (I have put more about Isabelle on this page). Isabelle language is two level allowing different types of logic to be used (the main one, used here, is higher order logic (HOL)), the inner language is enclosed in quotes:

locale semigroup =
  fixes f :: "'a => 'a => 'a" (infixl "*" 70)
  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"

locale abel_semigroup = semigroup +
  assumes commute [ac_simps]: "a * b = b * a"

lemma left_commute [ac_simps]:
  "b * (a * c) = a * (b * c)"
proof -
  have "(b * a) * c = (a * b) * c"
    by (simp only: commute)
  then show ?thesis
    by (simp only: assoc)


locale monoid = semigroup +
  fixes z :: 'a ("1")
  assumes left_neutral [simp]: "1 * a = a"
  assumes right_neutral [simp]: "a * 1 = a"

locale comm_monoid = abel_semigroup +
  fixes z :: 'a ("1")
  assumes comm_neutral: "a * 1 = a"

sublocale comm_monoid < monoid proof
qed (simp_all add: commute comm_neutral)

Again this language has function signatures (curryed like this "'a => 'a => 'a" Isabell is based on ML and sometimes requires ML code to be embedded into the Isabelle language).

Although Isabelle allows axioms to be specified, the specification of axioms using equations is dicouraged. In Isabelle an equals character '=' represents 'iff' (If and only if). Instead Isabelle uses a 'definitional approach' but not quite as arbitary computer code (algorithmns) such as is used in FriCAS code instead Isabelle encourages a more structured approac to building up definitions. These definitions then relate back to first principles.

Isabelle has a few built in datatypes and allows us to build up more complicated datatypes (including recursive definitions). The difference is Isabelle adds proofs to this, so recursive datatypes have the capability for inductive proofs.

The concepts of HOL come from an earlier language 'LCF' its key ideas are:

The ML family of languages are all decended from LCF.

The reason that equational definition of axioms is discouraged is that an arbitrary axiom, such as: f(x) + 1 = f(x), could lead to contradictions. For instance, if it were combined with a cancellation law we could derive 1=0.


Another interesting theorem prover is COQ which is based on constructive logic rather than HOL. COQ supports dependant types.

Axioms in Axiom

I have put further thoughs about representing axioms in a CAS like Axiom on this page.

Other Computer Algebra Programs

There is a wider list on this page:
Here are my own comments on some of them:





Covers a wide range of algebras, includes equation solvers.


Steep learning curve, need to learn SPAD language, very poor error messages, no IDE environment, no direct access to class library.


SPAD/Aldor - written in mixture of lisp and C.



Can program in Haskell environment.


Non-standard open source licence.
Does not cover such a wide range of algebras as Axiom.




Universal Algebra Calculator - a more specialised program just for universal algebra.





This is an internal DSL (Domain Specific Language) for Scala and so users have full access to Java environment.


Only supports numeric programming.




Includes a library for parsing lambda calculus, but not a general mathematics language program.



Java Algebra System



Java and Java Python






discrete algebra
no longer supported


Own Language






metadata block
see also:
  • I have put further thoughs about representing axioms in a CAS like Axiom on this page.
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.