> 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. _______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
