Long term goals: For your amusement :-)
9 views
Skip to first unread message
Tim Daly
May 26, 2026, 10:18:55 AM (19 hours ago) May 26
to FriCAS - computer algebra system
The Hawaii Test. Ah, how dreams die.
If you haven't seen this you might find it amusing.
It would be interesting to know what are the Fricas long term goals.
If you raise your eyes to the horizon, where are you going? Why?
This is from (axiom/goals in git):
Computational Mathematics is not a competition, it is a field
of study. Do what you can to make it better for all.
Axiom has several goals.
1) Axiom needs to live.
Keeping Axiom alive is a primary goal. It is patently obvious that
open source projects tend to die when the lead maintainer stops
development for any reason. Github and Sourceforge have many
thousands of examples.
Commercial software dies when the company dies. Witness
Symbolics (Macsyma), Soft Warehouse (Derive), or MapleSoft
(Maple was sold to a Japanese company which currently
supports it). Companies die, on average, after 15 years.
Axiom is timeless in that it is computational mathematics. The
algorithms and results will always be correct. So unlike other
efforts, what we write can be used by later generations.
This goal influences every decision about direction and purpose,
in particular, driving some of the goals listed below.
2) Axiom needs to be better documented and better explained.
The decision to deeply explain and document Axiom is based on
the obvious need to make it possible for new people to maintain,
modify, and extend it.
Explanation needs structure so a new person can "linearly learn"
what is needed. It also needs structure so information can be found
easily through some search mechanism. It further needs structure to
incorporate what is already known.
Literate programming was chosen after a long search for possbile
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 history.
Books are structure we understand.
You can find information in the volume choice; there are currently
21; the table of contents, tables of figures and subjects, detailed
indexes, a new "rich form bibliography" which includes abstracts,
and the use of hyperlinks between volumes, to outside sources,
and to youtube videos and courses. Experiments are being done
to embed gifs to illustrate ideas.
Algorithms, Categories, and Domains now have hyperlinks to
published literature and there are some initial examples of deeper
documentation of the algorithms. Ideally every algorithm will provide
sufficient explanation of the implementation or links to explanations
so the implementation can be understood in context.
In additon, people have generously contributed material from other
sources which directly explain details of Axiom, sometimes even
written by the Axiom primary authors.
There is a structured bibliography based on various sub-topics as
well as a section on external references to Axiom (currently 636
have been found).
There is an automated regression test suite that is being expanded
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 generation of help files.
Finally there is a literate bug document that points at known
problems (with a plan for adding deeper explanations and possible
solutions).
3) Axiom is RESEARCH software.
It is exploring ways to push the boundaries of computational
mathematics.
3A) Proving Axiom Correct
Computational Mathematics IS Mathematics.
It needs proofs, not handwaving.
This effort involves adding proof technology to Axiom.
Propositions are types and can be incorporated into the Category
structure as "type signatures". Domains already have
representations which is known in logic as the "carrier". 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 the
logic structure of "typeclasses" which have (signatures, carriers,
proofs) so there is a solid formal basis in logic for Axiom's
Category/Domain structure.
Because Axiom uses Group Theory as a scaffold there is a solid
formal basis for inheriting propositions 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 detail at a new system called LEAN.
3B) Number representations
There are two research efforts. One involves "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.
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
eliminate some of the costly checking and arrive a reliable results.
Some of this work is being done on a FPGA (which is now
mainstream on some Intel chips).
3C) Provisos
Provisos are a long-standing 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 greatly 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 coursework necessary for teaching
computational mathematics. There are Universities 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 under
a youtube channel for distance learning.
Besides computational mathematics, one of the courses will focus
on maintaining, modifying, and extending Axiom with new ideas.
5) Standards
5A) Axiom has done some work to automate the semantics of
NIST's Digital Library of Mathematical Functions (DLMF). Macros
translate the Latex sources to Axiom input based on additional
decorations.
5B) Axiom has a Computer Algebra Test Suite (CATS) which
uses published sources as test cases, finding bugs in Axiom
as well as the publications.
5C) Axiom is moving to full browser-based HTML5 documentation,
moving the 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 implementation of Clifford
algebra, are "in-process". Gustafson Floats will eventually be
another Domain as a numeric category, useful for constructing
things like POLY(GUST), that is, Polynomials over Gustafson floats.
New algorithms are interesting but without proper explanation of the
idea and the implementation detail they are just "soon-to-be-dead-code".
Every effort is being made to ensure that new code provides the details
needed to understand the algorithm and the implementation, along with
proper testing, examples, help files, and associated external references.
7) The 30 Year Horizon
Axiom has a "30 Year Horizon" focus. We will arrive at our goal in 30
years, starting today. Which is, in mathematical fashion, true for every
given future day.
Computational Mathematics is a huge field and we are only at the very
beginning of this journey. Find an idea. Research the literature. Talk to
a lot of people. Push the envelope just a little bit. In other words, do the
equivalent of a PhD thesis. You already have a research platform. You
don't need the degree, you just need the ambition.
Collaborate, Cooperate, Contribute.
of study. Do what you can to make it better for all.
Axiom has several goals.
1) Axiom needs to live.
Keeping Axiom alive is a primary goal. It is patently obvious that
open source projects tend to die when the lead maintainer stops
development for any reason. Github and Sourceforge have many
thousands of examples.
Commercial software dies when the company dies. Witness
Symbolics (Macsyma), Soft Warehouse (Derive), or MapleSoft
(Maple was sold to a Japanese company which currently
supports it). Companies die, on average, after 15 years.
Axiom is timeless in that it is computational mathematics. The
algorithms and results will always be correct. So unlike other
efforts, what we write can be used by later generations.
This goal influences every decision about direction and purpose,
in particular, driving some of the goals listed below.
2) Axiom needs to be better documented and better explained.
The decision to deeply explain and document Axiom is based on
the obvious need to make it possible for new people to maintain,
modify, and extend it.
Explanation needs structure so a new person can "linearly learn"
what is needed. It also needs structure so information can be found
easily through some search mechanism. It further needs structure to
incorporate what is already known.
Literate programming was chosen after a long search for possbile
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 history.
Books are structure we understand.
You can find information in the volume choice; there are currently
21; the table of contents, tables of figures and subjects, detailed
indexes, a new "rich form bibliography" which includes abstracts,
and the use of hyperlinks between volumes, to outside sources,
and to youtube videos and courses. Experiments are being done
to embed gifs to illustrate ideas.
Algorithms, Categories, and Domains now have hyperlinks to
published literature and there are some initial examples of deeper
documentation of the algorithms. Ideally every algorithm will provide
sufficient explanation of the implementation or links to explanations
so the implementation can be understood in context.
In additon, people have generously contributed material from other
sources which directly explain details of Axiom, sometimes even
written by the Axiom primary authors.
There is a structured bibliography based on various sub-topics as
well as a section on external references to Axiom (currently 636
have been found).
There is an automated regression test suite that is being expanded
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 generation of help files.
Finally there is a literate bug document that points at known
problems (with a plan for adding deeper explanations and possible
solutions).
3) Axiom is RESEARCH software.
It is exploring ways to push the boundaries of computational
mathematics.
3A) Proving Axiom Correct
Computational Mathematics IS Mathematics.
It needs proofs, not handwaving.
This effort involves adding proof technology to Axiom.
Propositions are types and can be incorporated into the Category
structure as "type signatures". Domains already have
representations which is known in logic as the "carrier". 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 the
logic structure of "typeclasses" which have (signatures, carriers,
proofs) so there is a solid formal basis in logic for Axiom's
Category/Domain structure.
Because Axiom uses Group Theory as a scaffold there is a solid
formal basis for inheriting propositions 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 detail at a new system called LEAN.
3B) Number representations
There are two research efforts. One involves "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.
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
eliminate some of the costly checking and arrive a reliable results.
Some of this work is being done on a FPGA (which is now
mainstream on some Intel chips).
3C) Provisos
Provisos are a long-standing 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 greatly 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 coursework necessary for teaching
computational mathematics. There are Universities 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 under
a youtube channel for distance learning.
Besides computational mathematics, one of the courses will focus
on maintaining, modifying, and extending Axiom with new ideas.
5) Standards
5A) Axiom has done some work to automate the semantics of
NIST's Digital Library of Mathematical Functions (DLMF). Macros
translate the Latex sources to Axiom input based on additional
decorations.
5B) Axiom has a Computer Algebra Test Suite (CATS) which
uses published sources as test cases, finding bugs in Axiom
as well as the publications.
5C) Axiom is moving to full browser-based HTML5 documentation,
moving the 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 implementation of Clifford
algebra, are "in-process". Gustafson Floats will eventually be
another Domain as a numeric category, useful for constructing
things like POLY(GUST), that is, Polynomials over Gustafson floats.
New algorithms are interesting but without proper explanation of the
idea and the implementation detail they are just "soon-to-be-dead-code".
Every effort is being made to ensure that new code provides the details
needed to understand the algorithm and the implementation, along with
proper testing, examples, help files, and associated external references.
7) The 30 Year Horizon
Axiom has a "30 Year Horizon" focus. We will arrive at our goal in 30
years, starting today. Which is, in mathematical fashion, true for every
given future day.
Computational Mathematics is a huge field and we are only at the very
beginning of this journey. Find an idea. Research the literature. Talk to
a lot of people. Push the envelope just a little bit. In other words, do the
equivalent of a PhD thesis. You already have a research platform. You
don't need the degree, you just need the ambition.
Collaborate, Cooperate, Contribute.
Tim Daly
May 26, 2026, 11:01:28 AM (18 hours ago) May 26
to fricas...@googlegroups.com
Even more amusing is that I have written several programs recently
using Claude Code. I haven't even looked at the generated source code.
Indeed one of the systems now just generates binary without code.
So clearly I have no idea what I'm talking about. History is harsh. :-)
The goal these days is to communicate from machine to machine
not human to human. The task is to create "skills", essentially
sets of prompts that focus the LLMs attention and indicate goals
for agents. For example,
Currently nobody actually understands how LLMs reach a conclusion
despite displaying "internal thoughts". Robots using VLA (vision language
action) perform actions that are so automatic they don't show up in the
internal thoughts trace.
I suspect that within a few years the hand-coded algorithm approach
will be pointless. Once the AI begins to deeply understand Trager's
Integration there is no need for code.
If you still write code by hand you're losing to history. The future arrived.
Write skills that "embody" computer algebra.
Tim
--
You received this message because you are subscribed to a topic in the Google Groups "FriCAS - computer algebra system" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/fricas-devel/iSKff3NyqFM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to fricas-devel...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/fricas-devel/8fd7d9eb-42c8-411e-90cc-a7f85784b522n%40googlegroups.com.
Qian Yun
May 26, 2026, 7:26:10 PM (10 hours ago) May 26
to fricas...@googlegroups.com
On 5/26/26 10:18 PM, Tim Daly wrote:
>
> It would be interesting to know what are the Fricas long term goals.
> If you raise your eyes to the horizon, where are you going? Why?
>
The README lists:
>
> It would be interesting to know what are the Fricas long term goals.
> If you raise your eyes to the horizon, where are you going? Why?
>
- continue structural improvements
(remove dead code, simplify code structure when possible)
- add new mathematical algorithms
(this goal will never be finished)
- develop better user interface
(needs better CLI, emacs interface, native GUI, web UI)
- develop improved Spad compiler
(hopefully Spad compiler is bootstrapped by Spad)
- make it easier for external programs to interface with FriCAS
(especially sagemath. The call-lisp-from-c interface seems brittle.)
- support for using external mathematical routines from Spad
(e.g. flint.)
From my side, goals/dreams:
fricas has fixed around 1000 bugs, maybe another few thousands
left to fix.
Some structural changes to avoid unsoundness.
Implement the missing pieces of Risch algorithm.
Once Spad compiler is bootstrapped, add backends to target
other languages.
Higher performance, multi-threading, SIMD, GPU even.
Make the architecture modular: core + extensions.
So that it is easier to understand, both by humans and AI.
- Qian
Qian Yun
May 26, 2026, 7:29:17 PM (10 hours ago) May 26
to fricas...@googlegroups.com
On 5/26/26 11:00 PM, Tim Daly wrote:
> Even more amusing is that I have written several programs recently
> using Claude Code. I haven't even looked at the generated source code.
> Indeed one of the systems now just generates binary without code.
> So clearly I have no idea what I'm talking about. History is harsh. :-)
>
> The goal these days is to communicate from machine to machine
> not human to human. The task is to create "skills", essentially
> sets of prompts that focus the LLMs attention and indicate goals
> for agents. For example,
> https://github.com/human-avatar/skills-for-humanity <https://github.com/
> Even more amusing is that I have written several programs recently
> using Claude Code. I haven't even looked at the generated source code.
> Indeed one of the systems now just generates binary without code.
> So clearly I have no idea what I'm talking about. History is harsh. :-)
>
> The goal these days is to communicate from machine to machine
> not human to human. The task is to create "skills", essentially
> sets of prompts that focus the LLMs attention and indicate goals
> for agents. For example,
> human-avatar/skills-for-humanity>
>
What about machine to human?
Do you think LLMs can understand Axiom? Can it help people
to complete the goal of document Axiom in literature programming
style? So that humans can understand Axiom completely?
- Qian
Hill Strong
May 26, 2026, 8:39:22 PM (9 hours ago) May 26
to fricas...@googlegroups.com
LLMs understand nothing and never can. At best, these systems are partial pattern recognisers and at worse the results are garbage.
What we see today is the same effect that occurred when database technology became common. People of all stripes including DBAs and other technical people had a trust of the technology which was unwarranted.
I have spent many many years having to analyse software systems and the vast majority are, how shall I put this, not doing what they are supposed to be designed for. The results obtained may appear to be correct. However, on deep analysis of the code base, one realises that the results obtained aren't real.
If one using any LLM has a detailed understanding of the code related to the specific LLM system, one can use that system somewhat effectively. Otherwise, one will face certain problems with whatever is produced.
I have found that subject matter experts are not necessarily au fait with the problems of the systems they use or build and trust those systems more than they should.
Mind you, most non-subject matter experts are worse in the trust they have for these systems.
One should trust these systems like you would a politician or a used car salesman or anyone trying to sell you a bridge in New York City.
I am not saying that one should never use these systems, but be very very very careful about trusting the results obtained. Check and recheck the results very very thoroughly before accepting those results.
- Qian
--
You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email to fricas-devel...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/fricas-devel/2ee4746e-e977-4145-a7d1-9eabc6df83e5%40gmail.com.
Tim Daly
12:45 AM (5 hours ago) 12:45 AM
to fricas...@googlegroups.com
> Do you think LLMs can understand Axiom? Can it help people
> to complete the goal of document Axiom in literature programming
> to complete the goal of document Axiom in literature programming
> style? So that humans can understand Axiom completely?
Barry Trager sent me a copy of the book "Integration in Finite Terms:
Fundamental Sources"[0]. The book has a series of papers leading up
to his PhD thesis. Years ago I tried several times to read and understand
his PhD work in integration and failed completely. Now I am working
through the background material.
While working through the book I revisited the resultant algorithm.
I asked an LLM about it. The result was
"When integrating rational functions, finding the logarithmic part of the
integral requires determining the poles and their associated residues.
Computing these algebraically without finding the roots of large
denominator polynomials requires the Rothstein-Trager Resultant."
Pulling on that thread leads to Barry's Masters Thesis.
I asked an LLM to explain the resultant algorithm. The LLM not
only explained it in great detail (I'm a slow learner), it constructed
many examples until I could compute it by hand.
That leads to WHY you need the resultant algorithm which leads
to further LLM question-answer sessions.
Without LLMs I'm not sure I could fully understand Trager in any
reasonable amount of time.
The point is that the LLMs can already explain Trager. The question
then becomes "When can they use that understanding to compute
integration". My guess is it already can when given the correct series of
prompts.
I had advocated developing an MCP (Model Context Protocol) server
to give LLMs access to the computer algebra system, part of the goal
of making the algebra available to other systems. However I think the
time has passed when this is useful. The LLMs already "know" most
of the answers to computer algebra questions. Whether the answer is
correct or not is questionable at the moment but I think that will change.
It would be an interesting study to discover how much computer algebra
system output is already "known" to an LLM. The LLM output requires
careful prompt construction (known as "skills"). I suspect the likely path
going forward will be constructing "skills" that give the same or better
output than the current computer algebra systems. It has the added
feature of being able to explain the result (aka machine-to-human) in
any desired amount of detail.
So the forward-looking path is "skill development" rather than hand
written algorithms. I am trying hard to learn this new game.
As the Red Queen in Carroll's "Through the Looking-Glass" said:
"Now, here, you see, it takes all the running you can do, to keep in
the same place. If you want to get somewhere else, you must run
at least twice as fast as that!"
Tim, the trailing edge runner.
[0] Clemens G. Raab and Michael F. Singer (ed)
"Integration in Finite Terms: Fundamental Sources" (2022) ISBN 9783030978664
You received this message because you are subscribed to a topic in the Google Groups "FriCAS - computer algebra system" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/fricas-devel/iSKff3NyqFM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to fricas-devel...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/fricas-devel/CAEnaMTGw6FpGs1MQTCCZxxRwqh30YP4xb31ijzsW%3D5%3Dahc%3DuEA%40mail.gmail.com.
Reply all
Reply to author
Forward
0 new messages