GPT4 and computer algebra

79 views
Skip to first unread message

Tim Daly

unread,
Jan 15, 2024, 8:10:37 AM1/15/24
to FriCAS - computer algebra system
"When integrated with tools such as formal proof verifiers,
internet search, and symbolic math packages, I expect, say,
2026-level AI, when used properly, will be a trustworthy
co-author in mathematical research, and in many other fields
as well" -- Terrance Tao

I might add that it would be important that the computer algebra
algorithms be proven correct.

Hill Strong

unread,
Jan 15, 2024, 5:45:52 PM1/15/24
to fricas...@googlegroups.com
No artificial stupidity (AI) will ever or should ever be considered as [a trustworthy co-author in mathematical research]. At best, these systems could be a possibly useful tool in the hands of those who know their subject field. In the hands of everyone else they will be like young children using power tools - a dangerous proposition at best and an utter disaster at worse.

There is far too much unthinking hype about the subject even by the researchers in the field.

--
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 on the web visit https://groups.google.com/d/msgid/fricas-devel/11e29cc8-7c91-4ad2-a56b-d380db9a33e3n%40googlegroups.com.

Dima Pasechnik

unread,
Jan 15, 2024, 6:59:46 PM1/15/24
to fricas...@googlegroups.com
On Mon, Jan 15, 2024 at 10:45 PM Hill Strong <elders...@gmail.com> wrote:
>
> No artificial stupidity (AI) will ever or should ever be considered as [a trustworthy co-author in mathematical research]. At best, these systems could be a possibly useful tool in the hands of those who know their subject field. In the hands of everyone else they will be like young children using power tools - a dangerous proposition at best and an utter disaster at worse.
>
> There is far too much unthinking hype about the subject even by the researchers in the field.

Well, we all know Doron Zeilberger's co-author:
https://sites.math.rutgers.edu/~zeilberg/ekhad.html

In this sense it's not new at all. More powerful, yes, but still...

>
> On Tue, 16 Jan 2024, 12:10 am Tim Daly, <axio...@gmail.com> wrote:
>>
>> "When integrated with tools such as formal proof verifiers,
>> internet search, and symbolic math packages, I expect, say,
>> 2026-level AI, when used properly, will be a trustworthy
>> co-author in mathematical research, and in many other fields
>> as well" -- Terrance Tao
>> https://youtu.be/3pb_-oLfWJ4?t=358
>>
>> I might add that it would be important that the computer algebra
>> algorithms be proven correct.
>>
>> --
>> 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 on the web visit https://groups.google.com/d/msgid/fricas-devel/11e29cc8-7c91-4ad2-a56b-d380db9a33e3n%40googlegroups.com.
>
> --
> 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 on the web visit https://groups.google.com/d/msgid/fricas-devel/CAEnaMTGr_Vk3qa-7X%3DVcPpmwuhEdcKySsngh1UaTmsTRgX9Lwg%40mail.gmail.com.

Hill Strong

unread,
Jan 15, 2024, 8:45:13 PM1/15/24
to fricas...@googlegroups.com
Agreed, not new at all. The Forbin Project 

To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/CAAWYfq36fDxKgk_wsx1g_Rx%3DaWWwv0uyKQHEpO5yBTbcEaNE9Q%40mail.gmail.com.

Tim Daly

unread,
Jan 15, 2024, 9:00:15 PM1/15/24
to FriCAS - computer algebra system
There is an interesting example of proof earlier in the video:

Reinforcement learning (using the Bellman equation[0]) needs
the ability to at least decide if it succeeds and can use information
about success in intermediate steps to rapidly improve. It also
needs a set of actions that can be performed at each step.
Reinforcement learning has conquered gaming with this structure.

LEAN provides a database of theorems, definitions, and tactics
that can be applied at each step of a proof. It provides feedback
about the local success of each action. It provides global success
once the proof completes. Thus all of the elements needed by
reinforcement learning are available in proof systems. LEAN's
theorems are strongly typed.

When training GPT-like systems, reinforcement training is the last
step (see Karpathy's slide 3):
It is straightforward to customize a GPT-like system with LEAN's
mathematical knowledge to focus on proofs.

We use group theory as our organizational skeleton. One of the steps
to integrating LEAN and computer algebra is aligning LEAN's axiom
structure with our category/domain structure (my current research).
Once that is done then theorems, such as a commutative theorem,
can be inherited and available to prove a function in a domain.

We use Buchberger's Groebner basis algorithm. This algorithm has
already been proven in Coq and is in use[1].

It is only a matter of time before the axioms which support the Risch
algorithm are proven. That will form the basis of proof of our current
implementation.

Because we are strongly typed and use a group theory scaffold we
are in a unique position to formalize our algorithms.

The combination of proof systems and computer algebra will be a
large step in computational mathematics.

Tim


[0] Bellman Equation

[1] Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics

Hill Strong

unread,
Jan 15, 2024, 10:05:54 PM1/15/24
to fricas...@googlegroups.com
Tim, notice though that the only intelligence here is what is provided by human intelligence. None of the various systems have any inherent intelligence.

My youngest granddaughter has just turned 1 and I have been spending time watching her develop intelligence and the difference between her and any of the current systems is possibly on the order of a million orders of magnitude with the systems being the primitive level.

As I said above, these systems can have possible use cases but only if humans are controlling them intelligently. It is a matter of finding specific use cases that work for us.

An appropriate analogy is summed up as: fire is a good servant but a destructive master.

To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/6ec0fcdb-1c96-4d5d-95df-35b52e3d97e1n%40googlegroups.com.

Tim Daly

unread,
Jan 16, 2024, 9:18:51 PM1/16/24
to FriCAS - computer algebra system
I have GPT systems running locally. It is possible to feed the systems
text files for training. Once trained they can answer questions related
to the training. It will be interesting to convert the book to text and
train the system on the book. At minimum it might make an interesting
"help" facility capable of responding to natural language questions.

Hill Strong

unread,
Jan 17, 2024, 2:05:44 AM1/17/24
to fricas...@googlegroups.com
Tim, 

That use should be something that would benefit people. Good luck with it.


Tim Daly

unread,
Jan 17, 2024, 7:09:14 AM1/17/24
to FriCAS - computer algebra system
I'm not the only one raising the question of AI and GPT systems and
their effects on Mathematics. The best and brightest of mathematicians,
of which I'm not one, are raising the issue.

This is a lecture by Jeremy Avigad,
Professor of Mathematics and Philosophy at CMU titled:
Is Mathematics Obsolete?

Timothy Gowers, a Fields Medalist, raises similar issues:
Can Computers Do Mathematical Research?

Gowers talks about computer proofs of mathematical theorems and
automatic mathematical reasoning. Gowers 'says that this may lead to a 
brief golden age, when mathematicians still dominate in original thinking 
and computer programs focus on technical details, “but I think it will last a 
very short time,” given that there is no reason that computers cannot eventually 
become proficient at the more creative aspects of mathematical research as well.'

Certainly, as I"ve mentioned, proof assistants provide all of the elements of
games which makes them perfect for reinforcement learning, the final
training stage of GPT systems. All this requires is a bright PhD candidate.

What few people so far have done is realize the impact this will have on
computer algebra. Certainly a GPT system can answer questions about
the proper handling of sqrt(4) and/or working through both the positive
and negative root assumptions in a calculation by conducting the calculation
applying the simplification for 2 and -2 and presenting both results. All the
GPT prompt would have to say is "assuming sqrt(4) is -2 compute ...".

The mixtral (Mixture of Experts)[0] system allows a custom expert to be
added to an existing system. A computer algebra expert is certainly possible.

This future is not far off. Consider that the ollama system[1] lists 61
systems, of which "wizard-math"[2] is one. The OpenAI "apps" page is
said to have several hundred systems since November 2023.

The jerk[3] in AI systems is difficult to track. Alvin Toffler[4] underestimated
the rapidity of change.  It is not a matter of "if", only a matter of "when".

Tim



[2] wizard-math "Model focused on math and logic problems"

[3] Jerk (Wikipedia) aka the third derivative
jerk ... is the rate of change of an object's acceleration over time

[4] Alvin Toffler "Future Shock"

Hill Strong

unread,
Jan 17, 2024, 9:17:09 AM1/17/24
to fricas...@googlegroups.com
Tim,

Some comments are below.

On Wed, Jan 17, 2024 at 11:09 PM Tim Daly <axio...@gmail.com> wrote:
I'm not the only one raising the question of AI and GPT systems and
their effects on Mathematics. The best and brightest of mathematicians,
of which I'm not one, are raising the issue.

They can raise the issue all they like. What they are not seeing is that artificial stupidity (AI) systems are limited. As I said above. The only intelligence you will find in these systems is the stuff generated by human intelligence. No artificial stupidity (AI) system can ever exceed the limitations of the programming entailed in them.
 

This is a lecture by Jeremy Avigad,
Professor of Mathematics and Philosophy at CMU titled:
Is Mathematics Obsolete?

Timothy Gowers, a Fields Medalist, raises similar issues:
Can Computers Do Mathematical Research?

Gowers talks about computer proofs of mathematical theorems and
automatic mathematical reasoning. Gowers 'says that this may lead to a 
brief golden age, when mathematicians still dominate in original thinking 
and computer programs focus on technical details, “but I think it will last a 
very short time,” given that there is no reason that computers cannot eventually 
become proficient at the more creative aspects of mathematical research as well.'

Here we see the failure of understanding the limitations found in all computer systems. We can build systems that can be used to develop proofs and may even be able to do exhaustive tests to find those proofs. But none of these systems will be able to do the original thinking that is inherent in human intelligence and intuition. I have been observing the many different areas in which we have progressed with computerised systems and the more I see, the more it becomes very clear that we will never get a thinking machine based on any level of technology that we are able to invent.

I said it in a previous comment above about watching my granddaughter as she is growing up. I have been watching my children and my grandchildren as well as many many other people. No matter how seemingly complex the systems we build, there is nothing that approaches even the animals, let alone humanity. Irrespective of any seeming intelligence that the researchers speak on, there is no intelligence within these systems. If you do ever see some artificial system show distinctive signs of real intelligence, take it that we are seeing a natural intelligence trying to fool you. There are many people who willingly commit fraud to achieve control over others.


Certainly, as I"ve mentioned, proof assistants provide all of the elements of
games which makes them perfect for reinforcement learning, the final
training stage of GPT systems. All this requires is a bright PhD candidate.

Proof assistants are relatively simple tools to help a human intelligence with the tedium involved. Nothing wrong with that as this is a useful amplification of our own abilities. But, we are far too stupid in reality to be able to understand what intelligence actually is. There are enough people, philosophers and theologians and physical scientists who are working on understanding this and we have in all essentials gotten nowhere in understanding what intelligence is, let alone understanding what we need to do to build anything even resembling the least of living intelligence systems.

I am far more concerned with what various people and groups of people will do with our current levels of technology than ever being concerned that we will ever build a real artificial system.

What seems to be lost is that we build real intelligence systems all the time and these we call children.


What few people so far have done is realize the impact this will have on
computer algebra. Certainly a GPT system can answer questions about
the proper handling of sqrt(4) and/or working through both the positive
and negative root assumptions in a calculation by conducting the calculation
applying the simplification for 2 and -2 and presenting both results. All the
GPT prompt would have to say is "assuming sqrt(4) is -2 compute ...".

The impact will be, if properly used, to build comprehensive proofs in mathematics that can have potential use in other areas of civilisation. But as we often see, the human motivations involved here are for the purposes of control, power and wealth and influence.

The insights that come from mathematics and how we can apply these are in all cases coming from our human intelligence.

One must be wary of the problem of the hype surrounding these systems. It is the case that we need to [follow the money] to see who gains from this hype.

All expert systems have points of failure that are never seen until far too late. These failure points are based on coding errors, data errors, human maliciousness, invalid assumptions and so on.

If anyone, no matter who it is, makes the assumption that we can build intelligent systems then they have fooled themselves and have forgotten that we are still far too primitive (as in caveman primitive) in regards to our technological advancement.

As for the rapidity of change, we forget the lessons of the past and are doomed to repeat them. In just 150 years, we have forgotten or discarded so much knowledge of what we could do.

Artificial systems can be used to correlate the enormous amounts of information that is still available, but it cannot correlate what we have already discarded and that information far exceeds what we have kept.

An example of the discard that has taken place is that some years ago, an emeritus professor at the University of Adelaide was contacted by a colleague of his from England. This colleague was involved in clearing out a closed down lab that hadn't been used in 60 -70 years. The emeritus professor took all the records in that lab and based on those records found an anomaly in of the extended Michelson-Morl;ey experiments. I believe the specific lab had been doing the experiment over a period of two years. None of this information had been published or was even known about. There are many different areas in which all sorts of experimental data and technology is now not available or at least no available in any electronic form.

All too often, people assume that our computer systems are reasonable and workably useful. To some extent they are. Often however, those useful reasonable results are only flukes. The actual code generating those results is utter garbage. If there is any serious complexity within these systems then there is a high likelihood that the system only has the appearance of being correct.

I have been looking at Metamath and it has a simplicity that allows for a good semblance of it being correct.

Axiom and FriCAS, as well as Maxima, Mathematics, SymPy and all the other associated systems are filled with [kludges] that cause interesting problems for the users of those systems. Artificial stupidity (AI) systems are even more unreliable. Without a human looking at the results of these systems.

That doesn't mean that useful work cannot be done, but you have to use these systems carefully and with understanding of the limitations involved in each. The work I have undertaken on rebuilding Axiom/FriCAS is to try and mitigate the underlying problems/features within these systems. Now, I have personal reasons for doing this and these reasons are in the furtherance of specific research areas I have in both quantum and non-quantum worlds based on a particular engineering mindset.

Always assume (and it is a fair assumption) that there is always one more bug in any code in any computerised systems, especially in any artificial stupidity system.

Note: I continue to use the term [artificial stupidity] because of the 40 years I have been involved in the various related areas.

At any rate enough of the rant from me. Have a blessed rest of the week as it comes to you.

Waldek Hebisch

unread,
Jan 17, 2024, 10:56:42 AM1/17/24
to fricas...@googlegroups.com
On Thu, Jan 18, 2024 at 01:16:55AM +1100, Hill Strong wrote:
> On Wed, Jan 17, 2024 at 11:09 PM Tim Daly <axio...@gmail.com> wrote:
>
> They can raise the issue all they like. What they are not seeing is that
> artificial stupidity (AI) systems are limited. As I said above. The only
> intelligence you will find in these systems is the stuff generated by human
> intelligence. No artificial stupidity (AI) system can ever exceed the
> limitations of the programming entailed in them.

Well, humans are at least as limited: your claim as true as claim
that "humans can not ever exceed the limitations of the programming
entailed in them". In case of humans programming meaning both things
hardcoded in genome and chemical machinery of the body and "learned
stuff". Already at age 1 toys, customized environment and interactions
with other humans make significant difference to learning. At later
stages there are stories which were perfected for thousends of years,
school curricula and books. There were myths that people from
non-western cultures are less "inteligent" than people from western
culture. More deeper research showed that part of our "inteligence"
is really "programmed" (learned) and "programming" in differnet
cultures were different.

In slightly different spirit, in fifties there were efforts to
define inteligence and researcheres from that time postulated
several abilities that every inteligent being should have.
Based on that there were "proofs" that artificial inteligence
is impossible. One of such "proofs" goes as follows: people
can prove math theorems. But Goedel and Church proved that
no machine can prove math theorem. So no machine will match
humans. The fallacy of this argument is classic abuse of
quantifiers: humans can prove same (easy) math theorems.
No machine or human can prove _each_ math theorem. Actually,
we still do not know how hard is proving, but common belief
is that complexity of proving is exponential in length of the
proof. What is proven is that that there is no computable
bound on length of shortest proof. Clearly this difficulty,
that is large length of proofs affect humans as much as
computers.

To put is differently, if you put strong requirements on
inteligence, like ability to prove each math theorem, then
humans are not inteligent. If you lower your requirements,
so that humans are deemed inteligent, than appropriately
programmed computer is likely to qualify.

One more thing: early in history of AI there was Eliza.
It was simple pattern matcher clearly having no inteligence,
yet it was able to fool some humans to belive that they
communicate with other human (ok, at least for some time).
Some people take this to consider all solved AI problems
as kind of fake and show that the problem was not about
inteligence. But IMO there is different possiblity: that
all our inteligence is "fake" in similar vein. In other
words, we do not solve general problem but use tricks which
happen to work in real life. Or to put it differently,
we may be much more limited than we imagine. Eliza clearly
shows that we can be easily fooled into assuming that
something has much more abilities than it really has
(and "something" may be really "we").

--
Waldek Hebisch

Bill Page

unread,
Jan 17, 2024, 1:57:13 PM1/17/24
to fricas...@googlegroups.com

On Wed, Jan 17, 2024 at 10:56 AM Waldek Hebisch <de...@fricas.org> wrote:
…

One more thing: early in history of AI there was Eliza.
It was simple pattern matcher clearly having no inteligence,
yet it was able to fool some humans to belive that they
communicate with other human (ok, at least for some time).
Some people take this to consider all solved AI problems
as kind of fake and show that the problem was not about
inteligence.  But IMO there is different possiblity: that
all our inteligence is "fake" in similar vein.  In other
words, we do not solve general problem but use tricks which
happen to work in real life.  Or to put it differently,
we may be much more limited than we imagine.  Eliza clearly
shows that we can be easily fooled into assuming that
something has much more abilities than it really has
(and "something" may be really "we").

+1

I strongly agree with your point in parenthesis above.  It seems to me that the current generation of AI tells us more about the actual capabilities of human beings and the nature of intelligence than it does about the limitations of computer systems.



Hill Strong

unread,
Jan 17, 2024, 10:03:53 PM1/17/24
to fricas...@googlegroups.com
Good morning Waldek,

My response will be delving into some areas of philosophical and metaphysical response.

On Thu, Jan 18, 2024 at 2:56 AM Waldek Hebisch <de...@fricas.org> wrote:
On Thu, Jan 18, 2024 at 01:16:55AM +1100, Hill Strong wrote:
> On Wed, Jan 17, 2024 at 11:09 PM Tim Daly <axio...@gmail.com> wrote:
>
> They can raise the issue all they like. What they are not seeing is that
> artificial stupidity (AI) systems are limited. As I said above. The only
> intelligence you will find in these systems is the stuff generated by human
> intelligence. No artificial stupidity (AI) system can ever exceed the
> limitations of the programming entailed in them.

Well, humans are at least as limited: your claim as true as claim
that "humans can not ever exceed the limitations of the programming
entailed in them".  In case of humans programming meaning both things

Though we are limited in every sort of way, we are capable of exceeding any programming that is involved in our development. What is so not obvious is that there is a category error when comparing humans to any sort of machine that we build. Though we can build machines stronger, faster and able to handle tedious tasks far better than we can do, due to our very distinctive intelligence, we are able to do what no machine can do and that is solve the problems that arise.


hardcoded in genome and chemical machinery of the body and "learned
stuff".  Already at age 1 toys, customized environment and interactions

You speak here about [programming] hard-coded in the genome and chemical machinery of the human body. But I somehow don't think you realise just how far beyond us is that machinery. Within a single living cell, the automatic adaptive capabilities are so far beyond our current levels of technology that in comparison, we are no more advanced than some caveman when we compare the entire planetary industrial and planetary capabilities that we have already made.

The more we learn about cellular biology with its internal transportation, control and manufacturing systems the more we should be recognising that we are not capable of building any computerised system that will ever be intelligent.

with other humans make significant difference to learning.  At later
stages there are stories which were perfected for thousends of years,
school curricula and books.  There were myths that people from
non-western cultures are less "inteligent" than people from western
culture.  More deeper research showed that part of our "inteligence"
is really "programmed" (learned) and "programming" in differnet
cultures were different.

Though part of our intelligence is learned there is something that is so far beyond this, so that, even though this is an active area of research, we haven't a clue as to what this is.


In slightly different spirit, in fifties there were efforts to
define inteligence and researcheres from that time postulated
several abilities that every inteligent being should have.
Based on that there were "proofs" that artificial inteligence
is impossible.  One of such "proofs" goes as follows: people
can prove math theorems.  But Goedel and Church proved that
no machine can prove math theorem.  So no machine will match
humans.  The fallacy of this argument is classic abuse of
quantifiers: humans can prove same (easy) math theorems.

Here you are now arguing against the various incompleteness theorems and in doing so, you are entering the realm of metaphysics and philosophy. These incompleteness theorems highlight something quite interesting in that the basis of our logic and mathematics (the fundamental axioms used) cannot be proved true from within our logic and mathematics. We can argue for them from metaphysics and philosophy but we are unable to prove them from within the systems that are based on those fundamental axioms.

What you have missed here is that any theorems developed within the systems are provable based on those unprovable axioms and previously proven theorems. That is how we can build up the various systems of mathematics in use. However, new mathematical systems require insights not possible to any computerised system. These new insights are in the realm of human intelligence which does exceed any programming that individual humans may be exposed to.

No machine or human can prove _each_ math theorem.  Actually,
we still do not know how hard is proving, but common belief

All theorems can be proved if they are based on the initial set of axioms used. How hard it is to prove the theorem is another matter. 
 
is that complexity of proving is exponential in length of the
proof.  What is proven is that that there is no computable
bound on length of shortest proof.  Clearly this difficulty,
that is large length of proofs affect humans as much as
computers.

Maybe. The thing of interest here is that it is humans who can find alternative ways of proving a theorem which is not a part of the exhaustive processes previously used.

As you would well know, the Halting problem is not solvable by any Turing machine or corresponding alternative. But we can see the problem immediately. We make leaps and find solutions that are not possible within a logical/mathematical system.


To put is differently, if you put strong requirements on
inteligence, like ability to prove each math theorem, then
humans are not inteligent.  If you lower your requirements,
so that humans are deemed inteligent, than appropriately
programmed computer is likely to qualify.

Your comment above is false. It is false logically, rationally, metaphysically and philosophically. The ability to prove a mathematics theorem, if based on previous axioms and theorems, is not a sign of intelligence. I would agree that we do this as a part of our intelligence, but this is not a sign of intelligence. The axioms used at the fundamental level which are designed and specified may well be a sign of intelligence, but no computerised system does this. I have spent 40 years looking at these kinds of things and every computerised system is based on the human intellectual capacity (intelligence) for these systems to even exist. 

One more thing: early in history of AI there was Eliza.
It was simple pattern matcher clearly having no inteligence,
yet it was able to fool some humans to belive that they
communicate with other human (ok, at least for some time).

The ability to fool people does not challenge our intelligence. Every human is flawed and can be fooled. We see that every day in every society. This does not lessen what humanity has in terms of being intelligent. We act irrationally, we act in completely adverse ways. We make decisions that make no sense. We even choose options that are not actually available to us. We can see this in the recent Iowa caucus where the winner wasn't even on the available options.

Machine programming doesn't allow this. Certainly, we can see all sorts of errors and when fully studied, we see why those errors occurred. They are logically defined.

Some people take this to consider all solved AI problems
as kind of fake and show that the problem was not about
inteligence.  But IMO there is different possiblity: that
all our inteligence is "fake" in similar vein.  In other

If our intelligence is [fake] then the logical consequence of that argument is that there is no mathematics, no scientific investigation, no rationality, no intelligence, no progress in any form. This is a contradiction. We do do mathematics, we do do scientific investigation, we do do philosophy and metaphysics, we do do rational things.

words, we do not solve general problem but use tricks which
happen to work in real life.  Or to put it differently,

Yes we do do tricks and this is one sign of intelligence here. Certainly we are limited and I have been saying such things for a long time. However, for all of our limitations, we are in a category that is very different to all other things, living or otherwise and we often fail to recognise, let alone understand that category difference.

I have seen too many people who dismiss philosophy and metaphysics as being useless. Yet it is by these that we show forth our intelligence and by which we can justify mathematics and scientific investigation as valid, rational and proper intellectual pursuits.


we may be much more limited than we imagine.  Eliza clearly
shows that we can be easily fooled into assuming that
something has much more abilities than it really has
(and "something" may be really "we").

--
                              Waldek Hebisch

--
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.

Tim Daly

unread,
Jan 18, 2024, 12:32:34 AM1/18/24
to FriCAS - computer algebra system
While the question of human intelligence is interesting
please note that my post topic has been restricted to the
application of GPT-like / AI-like systems to the automation
of proof and computer algebra.

Given the changes I'm seeing and the research I'm doing it
is likely that there will be a very rapid change from the legacy
version of computer algebra we now use, taking advantage of 
the growing power of these systems.

I've been involved and published in AI-like systems since the 1973, including such
"AI-like" areas of machine vision, robotics, expert systems, speech, neural
nets, knowledge representation, planning, etc. All of these were considered
"intelligent behavior" ... until they weren't. Indeed, in the 1960s computer
algebra-like systems were considered "intelligent".

Intelligence is a "suitcase word" [0], interesting but irrelevant.

The topic at hand is "computational mathematics", meaning the application
of recent technology (proof assistants, theorem databases, algorithm
proofs, and reasoning assistants) to moving beyond 50-year-old legacy
computer algebra. Proving computer algebra algorithms correct and
providing useful interfaces is the long-term goal.

Tim

[0] "Marvin Minsky, in his fascinating book "The Emotion Machine" ... described 
words such as "emotions," "memory," "thinking" and "intelligence" as suitcase 
words - words that mean "nothing by itself, but holds a bunch of things inside 
that you have to unpack."

Tim Daly

unread,
Jan 18, 2024, 1:49:46 AM1/18/24
to FriCAS - computer algebra system
AlphaGeometry: An Olympiad-level AI system for Geometry

Hill Strong

unread,
Jan 18, 2024, 1:55:40 AM1/18/24
to fricas...@googlegroups.com
Good afternoon Tim,

On Thu, Jan 18, 2024 at 4:32 PM Tim Daly <axio...@gmail.com> wrote:
While the question of human intelligence is interesting
please note that my post topic has been restricted to the
application of GPT-like / AI-like systems to the automation
of proof and computer algebra.

While such systems may (and I stress may) be useful in the hands of talented humans, it will require the insights of humans to use these systems properly. The problem is the use of the word [intelligence] in relation to these systems. It would be far better to use some other terms to show that these systems are tools first and formost.
 

Given the changes I'm seeing and the research I'm doing it
is likely that there will be a very rapid change from the legacy
version of computer algebra we now use, taking advantage of 
the growing power of these systems.

There is nothing wrong with taking advantage of these systems in this kind of work. But we must ensure that we don't attribute to these systems properties that are not true. 
 

I've been involved and published in AI-like systems since the 1973, including such
"AI-like" areas of machine vision, robotics, expert systems, speech, neural
nets, knowledge representation, planning, etc. All of these were considered
"intelligent behavior" ... until they weren't. Indeed, in the 1960s computer
algebra-like systems were considered "intelligent".

I agree with you that all of these systems have had associated with them the term [intelligent behaviour] and in hindsight this has been a major mistake and a detriment to our advancement of these systems.
 

Intelligence is a "suitcase word" [0], interesting but irrelevant.

Unfortunately not actually irrelevant.

The topic at hand is "computational mathematics", meaning the application
of recent technology (proof assistants, theorem databases, algorithm
proofs, and reasoning assistants) to moving beyond 50-year-old legacy
computer algebra. Proving computer algebra algorithms correct and
providing useful interfaces is the long-term goal.

I do not disagree with you here. However, it behooves us to ensure that appropriate terminology is used that does not get distorted once these systems enter into wider usage.
 

Hill Strong

unread,
Jan 18, 2024, 2:06:39 AM1/18/24
to fricas...@googlegroups.com
Tim,

This is a good example of the problem of the language we are using.

Tim Daly

unread,
Jan 18, 2024, 12:08:19 PM1/18/24
to FriCAS - computer algebra system
Jeremy Avigad has two youtube videos showing how strong these
interactive proof assistants have become:

Formal mathematics, dependent type theory, and the Topos Institute

The Design of Mathematical Language

It seems to me that it should be possible to encode the Risch algorithm proof.

Hill Strong

unread,
Jan 19, 2024, 4:10:46 AM1/19/24
to fricas...@googlegroups.com
Tim,

The first video is interesting for a number of reasons.

The first reason is that mathematicians don't like tedium and proof assistants can contribute to that tedium. (Formal mathematics part 18 -19 minute mark)

The next section on Teaching highlights an especially good reason for proof assistants and that is the confidence that we can have that the theorems being taught and used have been verified. Many times in my undergraduate engineering, we were introduced to various theorems relevant to the engineering subjects that we were being taught and it was assumed that the particular proofs for those theorems were correct. Yet, the problem that we were faced with was that it was assumed that any previous theorems used as a basis for the specific theorem being proved were true. In many cases we were not shown that those base theorems were in fact true. At that time, these tools were not available or were not known to be available. We were taught to be pragmatic and if these theorems were useful in practical ways, we used them. It has been in latter years that formal proofs for all theorems (especially in engineering)  has become a matter of interest and concern.

The next section on mathematical discovery concerns me. He is assuming that there is an underlying intelligence to these tools and in doing so fails to see that these are just tools that people can use to do what they need to do. He does recognise that pure mathematicians don't appear to have made a determination where or how these tools can be used and I think that is tied up with the baggage that there is intelligence in these tools. People and this includes mathematicians and scientists treat tools quite differently when they assume that the tools they are using have some level of intelligence. I have observed this strange change for well over 30 years and it is getting worse. Instead of using a tool as a tool and being in control of that tool, people start to defer to the tool if they have an idea that it has some level of intelligence. I see this happening with the general public and I see it happening with mathematicians and scientists.

I don't have a problem with automation per se. I have used automation to remove many tasks for people over the years. But I don't implicitly trust automation because I know just how fragile all such systems are and I try to endure that work-arounds are available in the event of failure.

His insight into formalism and collaboration is something that is often done but rarely appreciated in the main.

In his section on Dependent Types, there is an implicit problem underlying his discussion on type checking. Interestingly, this particular subject was being researched and discuss in the late 1970's to the mid 1980's at the University of St Andrews in the Computer Science departments. What it boiled done to was that certain type checking was only decidable at runtime and not at compile time. Interestingly, type checking became one of those inane and often vitriolic discussions. The middle ground people who were of the opinion to use both static and runtime typing were the target of both sides of the argument. It is well known that compile time type checking is undecidable in certain circumstances and so such systems work to restrict what kinds of type checking are allowed. This leads to certain classes of problems not being amenable to static type checking.

If you allow runtime type checking to be used as well, then the problems with static type checking in Dependent Type theory are mitigated.

His approach is based on purely static type checking even though there is an implication in what he says of a possible mitigation here.

In the section on types and expressions, at the end of that section, he makes a distinction between #eval and #check. There is no distinction here. You are evaluating expressions. The end result of those expressions are different, no issue with that. But both are evaluations of expressions. I find making the distinction here to be somewhat problematic and complicates the discussion where there should be no such complication. This is the same kind of complication that has arisen in the static/dynamic type checking arguments.

This is enough comment at this time.

Tim Daly

unread,
Jan 20, 2024, 4:23:18 AM1/20/24
to FriCAS - computer algebra system
Alpha Everywhere: AlphaGeometry, AlphaCodium, and the Future of LLMs

It appears that these Alpha* systems are using an architecture where the
LLM proposes possible ideas and the solution machinery grinds out a
success or failure. On failure the LLM generates new ideas and the
cycle continues.

AlphaGeometry uses this during theorem proving which makes me think
it could be applied to LEAN's proof work.

In some sense this bypasses Godel's limitations. The LLM is using
information gathered from the world which is inconsistent at best,
wrong at worst, but occasionally useful as a "bypass technique".

Note that these systems are being released as open source so
I'll likely to be spending time getting them running.
Reply all
Reply to author
Forward
0 new messages