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.
