Re: [Axiom-developer] Axiom mathematical algorithms... Notation matters

[daly]

> Now that "Einstein's Apple" is in World Scientific's catalog,
> I'm waking up my interest things algebraic and AI-ish.
> 
> I seem to recall that you had some ideas for the help
> capabilities of AXIOM and have started burrowing through
> old notes to find what has been said.
> 
> Any comment on what you've had in mind?

Congrats on the new book. Books take a huge amount of work.

There are new additions and changes to Axiom's help.

For the )describe command, as in

)d op pop!

there are command line examples for using the function from each domain.
These are slowly being added to all of the functions.

Help pages for all categories, domains, packages, and numerics are now
automatically extracted and available to the )help command. Detailed
examples of function use is slowly being added to each one.

All of the algebra and, so far, most of the interpreter and compiler
are PDFs. The actual source code is extracted from the latex source
files. Bibliographic references are being added. A complete table of
contents volume now exists and will shortly have hyperlinks to the
referenced volume and section.

Each category, domain, package, and numerics will have an overview
and each function will have an explanation, examples, and a proof.

Axiom now automatically runs ACL2 (for lisp code) and COQ (for
algebra code) at build time to automate the proofs. A lisp function
has been proven and a COQ algebra function proof is "in-process".

Additional examples are being added to the src/input directory. These
will eventually be collapsed into a new volume showing Axiom use.

Axiom videos are "in plan". I have been experimenting with tools to
make videos. I have experimented with inlining videos and gifs into
the PDFs. So far, nothing has been pushed to the repositories.

================================================================


On the AI front I have sent the following proposal to several people.
I would work on it but I don't have access to the computer resources
necessary to train the deep neural net. But I think that we are
on the edge of solving hand-written input of mathematics.


Machine learning of labeled data can change mathematics.

Hand-written input to mathematics programs is a long-standing problem
in the mathematics community that gets unsuccessfully attacked every
few years. Many have tried, all have failed.

Hand-written mathematical input would open the world of symbolic
mathematics to researchers and students at all levels.

With machine learning and big data we can incrementally approach
a solution. The task breaks down into several steps, each of which
can be automated and can build on prior steps. 

Step 0 would be to build a labeled dataset of latex-typeset images.

These already exist. Axiom has a huge test suite at
http://axiom-developer.org/axiom-website/CATS
which include, for example, the Schaums Integration equations,
the Kamke ordinary differential equations, and the Rich integration
dataset. Many other such datasets exist or can easily be automated.
Indeed, the CRC publishes huge typeset math books from latex. This
would be a collection of data with labels.

These existing datasets group the latex input. the typeset equations,
and, in some cases, the Axiom input command lines. See page 4 of
http://axiom-developer.org/axiom-website/CATS/schaum1.input.pdf

What is missing is a way to extract the semantics of the image so
we can go from typeset equations to command lines.

Step 1 would be to recognize the typeset symbols like x, a, pi, theta
and categorize the input based on symbol set. Now we can recognize
the small set of mathematical symbols.

Step 2 would be to recognize symbol groupings such as fractions,
roots, integral signs, absolute values, and functions with arguments.

At this point we can recognize and generate the input that would
generate the output image. Now we can point a camera at an equation
in a textbook and generate the semantics. Knowing the semantics allows
automated input to symbolic mathematics.

There are two interesting "Step 3" paths.

Step 3 Path 1 automates integration, differential equations, and other
mathematics by using machine learning to associate the input equation
and the solution. Given an integral, a wave equation, or a
differential equation, we can recognize that it is as, say, a
"Bernoulli equation" (in one of many forms) with a known solution.

Step 3 Path 2 would explore recognizing handwritten symbols such as
x, a, pi, theta and categorize the input based on the symbol set.
Recognizing handwritten symbols is similar to the MNIST problem.
Then the symbol groupings would need to be recognized as above.

Success in either path would allow mathematicians and students to 
write equations on a tablet and use it as input to a symbolic
algebra system or as input to an "equation pattern matcher" to
suggest solutions.

Currently we expect people to use calculators so they can handle
larger problems while automating the rote tasks. We are at the
threshold of making equation handling into another rote task. This
will affect the teaching of mathematics worldwide.