Several people have asked about Axiom's goal=
s and about

my opinions on other free and commercial systems.=

I have no opinions about other free or commercial syste=
ms.

Computational Mathematics is not a competition, it i= s a field

of study. Do what you can to make it better for all=
.

Axiom has several goals.

Keeping Axiom alive is a primary goal. It is paten=
tly obvious that

open source projects tend to die when the le=
ad maintainer stops

development for any reason. Github and So=
urceforge have many

thousands of examples.

=
Commercial software dies when the company dies. Witness

Symbo=
lics (Macsyma), Soft Warehouse (Derive), or MapleSoft

(Maple =
was sold to a Japanese company which currently

supports it).=
Companies die, on average, after 15 years.

Ax=
iom is timeless in that it is computational mathematics. The

=
algorithms and results will always be correct. So unlike other

in particular, driving some of the goals listed below.

<=
div>2) Axiom needs to be better documented and better explained.The decision to deeply explain and document Axiom is based on

t= he obvious need to make it possible for new people to maintain,

modify,= and extend it.

t= he obvious need to make it possible for new people to maintain,

modify,= and extend it.

Explanation needs structure so a new pers=
on can "linearly learn"

what is needed. It also needs structu= re so information can be found

easily through some search mechanism. It= further needs structure to

incorporate what is already known.

<= /div>

The book-like nature of a literate program= focuses attention on

people, not machines. It is a linear format which= provides a way

to communicate ideas using methods developed over histo= ry.

Books are structure we understand.

You can find i= nformation in the volume choice; there are currently

21; the table of c= ontents, tables of figures and subjects, detailed

indexes, a new "= rich form bibliography" which includes abstracts,

and the use of h= yperlinks between volumes, to outside sources,

and to youtube videos an= d courses. Experiments are being done

--94eb2c1cd628f06ac60556dce1fb--

what is needed. It also needs structu= re so information can be found

easily through some search mechanism. It= further needs structure to

incorporate what is already known.

<= /div>

Literate programming was chosen after a long search for possbile =

solutions.

solutions.

The book-like nature of a literate program= focuses attention on

people, not machines. It is a linear format which= provides a way

to communicate ideas using methods developed over histo= ry.

Books are structure we understand.

You can find i= nformation in the volume choice; there are currently

21; the table of c= ontents, tables of figures and subjects, detailed

indexes, a new "= rich form bibliography" which includes abstracts,

and the use of h= yperlinks between volumes, to outside sources,

and to youtube videos an= d courses. Experiments are being done

to embed gifs to illust=
rate ideas.

Algorithms, Categories, and Domain=
s now have hyperlinks to

published literature and there are some initia= l examples of deeper

documentation of the algorithms. Ideally every alg= orithm will provide

sufficient explanation of the implementation or lin= ks to explanations

so the implementation can be understood in context.<= br>

published literature and there are some initia= l examples of deeper

documentation of the algorithms. Ideally every alg= orithm will provide

sufficient explanation of the implementation or lin= ks to explanations

so the implementation can be understood in context.<= br>

In additon, people have generously contributed=
material from other

sources which directly explain details of Axiom, s= ometimes even

written by the Axiom primary authors.

sources which directly explain details of Axiom, s= ometimes even

written by the Axiom primary authors.

T=
here is a structured bibliography based on various sub-topics as

well a= s a section on external references to Axiom (currently 636

well a= s a section on external references to Axiom (currently 636

h=
ave been found).

There is an automated regress=
ion test suite that is being expanded

and made uniform for testing all = known functions. The Axiom code

and made uniform for testing all = known functions. The Axiom code

is now using a uniform syntax=
and has per-function help text, as

well as automated generat=
ion of help files.

Finally there is a literate=
bug document that points at known

problems (with a plan for adding dee= per explanations and possible

solutions).

problems (with a plan for adding dee= per explanations and possible

solutions).

3) Axiom is=
RESEARCH software.

It is exploring ways to push the boundaries of = computational

mathematics.

It is exploring ways to push the boundaries of = computational

mathematics.

3A) Proving Axiom Correct<=
br>

Computational Mathematics IS Mathematics.

= It needs proofs, not handwaving.

= It needs proofs, not handwaving.

This effort involves add=
ing proof technology to Axiom.

Propositions are types and can be incorp= orated into the Category

structure as "type signatures". Doma= ins already have

representations which is known in logic as the "c= arrier". Proofs

of Propositions, using operations from the domain,= will show that

the Domain is properly designed and implemented.

Propositions are types and can be incorp= orated into the Category

structure as "type signatures". Doma= ins already have

representations which is known in logic as the "c= arrier". Proofs

of Propositions, using operations from the domain,= will show that

the Domain is properly designed and implemented.

The three parts (signatures, representations, proofs) mirror th=
e

logic structure of "typeclasses" which have (signatures, ca= rriers,

proofs) so there is a solid formal basis in logic for Axiom'= ;s

Category/Domain structure.

logic structure of "typeclasses" which have (signatures, ca= rriers,

proofs) so there is a solid formal basis in logic for Axiom'= ;s

Category/Domain structure.

Because Axiom uses Grou=
p Theory as a scaffold there is a solid

formal basis for inheriting pro= positions so a Domain knows what

it needs to prove and what operations = are needed in the Domain

to support that proof.

formal basis for inheriting pro= positions so a Domain knows what

it needs to prove and what operations = are needed in the Domain

to support that proof.

Axiom currently can invoke Coq and ACL2 during the build process.

An example of automatically proving a lisp algorithm using ACL2

exists= . A Coq example is being worked on. In addition, we are

looking in deta= il at a new system called LEAN.

An example of automatically proving a lisp algorithm using ACL2

exists= . A Coq example is being worked on. In addition, we are

looking in deta= il at a new system called LEAN.

3B) Number re=
presentations

There are two research efforts. One involve=
s "formal numbers" so

that we can claim that the symbol '= x' is an 'Integer' without giving

it a value. This was work= originally performed under grant at City

College of New York.

<= /div>

**Every effort is being made to ensure that new code provides the details**

that we can claim that the symbol '= x' is an 'Integer' without giving

it a value. This was work= originally performed under grant at City

College of New York.

<= /div>

The second involves work by Gustafson on a new representation

of floats that can be dynamic in range and easier to reason about.

The= goal is to push this through the numeric libraries in order to

elimina= te some of the costly checking and arrive a reliable results.

Some of t= his work is being done on a FPGA (which is now

mainstream on some Intel= chips).

of floats that can be dynamic in range and easier to reason about.

The= goal is to push this through the numeric libraries in order to

elimina= te some of the costly checking and arrive a reliable results.

Some of t= his work is being done on a FPGA (which is now

mainstream on some Intel= chips).

3C) Provisos

Provisos are a long-standin= g research question. Some work has

been done, mostly using Cylindrical = Algebraic Decomposition, to

derive new ways to constrain the boundaries= of valid computations.

It is expected that this work will benefit grea= tly from the integration

with formal methods listed above.

Besides computational mathematics, one of the courses will focus

on = maintaining, modifying, and extending Axiom with new ideas.

Provisos are a long-standin= g research question. Some work has

been done, mostly using Cylindrical = Algebraic Decomposition, to

derive new ways to constrain the boundaries= of valid computations.

It is expected that this work will benefit grea= tly from the integration

with formal methods listed above.

4) Teaching

In order to keep Axiom alive we need to=
teach the next generation.

Axiom is developing the cours=
ework necessary for teaching

computational mathematics. There are Unive= rsities planning to

teach using Axiom and every effort will be made to = support those

efforts. In addition, there is a plan to teach at CMU.

computational mathematics. There are Unive= rsities planning to

teach using Axiom and every effort will be made to = support those

efforts. In addition, there is a plan to teach at CMU.

The end result will be course outlines, a set of slides for=
standard

28 lecture courses, and published youtube videos collected un= der

a youtube channel for distance learning.

28 lecture courses, and published youtube videos collected un= der

a youtube channel for distance learning.

on = maintaining, modifying, and extending Axiom with new ideas.

<=
br>

5) Standards

5A) Axiom has done some work t=
o automate the semantics of

NIST's Digital Library of Mathematical = Functions (DLMF). Macros

translate the Latex sources to Axiom input bas= ed on additional

decorations.

NIST's Digital Library of Mathematical = Functions (DLMF). Macros

translate the Latex sources to Axiom input bas= ed on additional

decorations.

5B) Axiom has a Compute=
r Algebra Test Suite (CATS) which

uses published sources as test cases,= finding bugs in Axiom

as well as the publications.

uses published sources as test cases,= finding bugs in Axiom

as well as the publications.

5=
C) Axiom is moving to full browser-based HTML5 documentation,

moving th= e Hypertex and Graphics packages to HTML and Canvas

code. Dynamic Axiom= input/output in HTML exists and works.

moving th= e Hypertex and Graphics packages to HTML and Canvas

code. Dynamic Axiom= input/output in HTML exists and works.

6) New Algorithms=

Research on new algorithms, such as a full implementatio=
n of Clifford

algebra, are "in-process". Gustafson =
Floats will eventually be

another Domain as a numeric category, useful f= or constructing

things like POLY(GUST), that is, Polynomials over Gusta= fson floats.

another Domain as a numeric category, useful f= or constructing

things like POLY(GUST), that is, Polynomials over Gusta= fson floats.

New algorithms are interesting b=
ut without proper explanation of the

idea and the implementat=
ion detail they are just "soon-to-be-dead-code".

needed to understand the algorithm and the implementation, alo=
ng with

proper testing, examples, help files, and associated =
external references.

7) The 30 Year Horizon

Axiom has a "30 Year Horizon" focus.=C2=A0 We wil=
l arrive at our goal in 30

years, starting today. Which is, i=
n mathematical fashion, true for every

given future day.

<=
div>Computational Mathematics is a huge field and we are only at the verygiven future day.

beginning of this journey. Find an idea. Research the literatu=
re. Talk to

a lot of people. Push the envelope just a little =
bit. In other words, do the

equivalent of a PhD thesis. You a=
lready have a research platform. You

don't need the degree, you jus= t need the ambition.

don't need the degree, you jus= t need the ambition.

Collaborate, Cooperate, Contribute.<=
br>

Tim

=C2=A0

=C2=A0