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. On Tue, 16 Jan 2024, 1:00 pm Tim Daly, <[email protected]> wrote: > There is an interesting example of proof earlier in the video: > https://youtu.be/3pb_-oLfWJ4?t=298 > > 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): > https://karpathy.ai/stateofgpt.pdf > 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 > https://en.wikipedia.org/wiki/Bellman_equation > > [1] Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, > Geometry and Arithmetics > https://arxiv.org/abs/1007.3615 > > > > > > On Monday, January 15, 2024 at 6:59:46 PM UTC-5 Dima Pasechnik wrote: > >> On Mon, Jan 15, 2024 at 10:45 PM Hill Strong <[email protected]> >> 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, <[email protected]> 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 [email protected]. >> >> 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 [email protected]. >> > To view this discussion on the web visit >> https://groups.google.com/d/msgid/fricas-devel/CAEnaMTGr_Vk3qa-7X%3DVcPpmwuhEdcKySsngh1UaTmsTRgX9Lwg%40mail.gmail.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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/fricas-devel/6ec0fcdb-1c96-4d5d-95df-35b52e3d97e1n%40googlegroups.com > <https://groups.google.com/d/msgid/fricas-devel/6ec0fcdb-1c96-4d5d-95df-35b52e3d97e1n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/CAEnaMTHv7jRyBZEhbtLYLyiQa62WKDOcj9K95wS6dAtYus3zEg%40mail.gmail.com.
