This will be a bit long but ... I'm working to combine Axiom and LEAN. LEAN is a CMU/MS project[0][1] They have a proof assistant and a rapidly growing database of theorems and proofs. The whole database (mathlib[2]) is strongly typed so it is easy to know if a theorem applies to a step in your proof. They have a program which will show a graph of dependency graph of each proof so it is clear what proof depends on what axiom/proof/definition.
I want to prove the algorithms used in Axiom. Buchberger's Groebner basis algorithm has already been formally proven (attached). I am working on a proof hierarchy parallel to the category/domain hierarchy. Proofs of group theory theorems are attached to the corresponding Axiom categories. That way they get inherited by the domains. Functions in a domain can use the theorems and proofs to prove each domain function. Ultimately I'd like to see a proof of the Risch algorithm. I'm also deeply involved with AI. Most of my career is actually in the AI area. My Masters degree work was in machine vision and a lot of my jobs were in Robotics, including at Unimation, the company that invented Industrial Robots. I also authored Expert Systems software from IBM and done work at CMU to change a car tire with Human/Robot cooperation. These days I'm heavily involved with AI. I have 71 LLMs which I am benchmarking on their ability to do proofs. Most of them already can. The basic research goal is to use AI techniques to automate proofs. Historically this has been a nonsense idea. The basic argument is that the only effective method was enumerating possible next steps. This leads to a combinatorial explosion. So, the argument goes, there is no possible automated solution. Several things have changed. First, reinforcement learning has shown that it can be trained to play any game (chess, go, video games, etc). It requires STATES (the current state of the play), ACTIONS (what moves can be made in each state), SUCCESS/FAIL feedback (either only at the end of the game or on each step if that is available). Second, LEAN has developed an IDE that maintains STATES. It will show you where you are in the proof. It will manage multiple branches so you can work on any one branch at a time. LEAN provides ACTIONS. Either a proof applies or there are programs called tactics which automate a lot of the steps needed to move the proof ahead. The important part is that each LEAN theorem / tactic is strongly typed which severely limits the available actions. Notice that this undercuts the combinatorial explosion argument. LEAN provides SUCCESS/FAIL feedback. It can keep track of what branches of a proof are complete and which are still open. It provides SUCCESS when the proof is complete. So all of the elements required for reinforcement learning already exist in LEAN. Viewed as a game, LEAN proofs can be automated. Also of note, after the LLM AI systems are trained there is a final step called RLHF, Reinforcement Learning with Human Feedback. I intend to choose certain LLMs to already do proofs and train them on LEAN using reinforcement learning. I have collected the theorem / proofs from my Advanced Calculus college book[3] to use as new, unseen test cases. All of this is a subgoal of the larger goal of merging computer algebra and proof assistants to form "computational mathematics". These two fields of automated mathematics don't seem to talk. Of the hundreds of papers I've read only James Davenport is mentioned in the bibliography of both fields. All of that said, I will note that the latest Gemini 1.5 and GPT4.2 are so much more powerful than the LLMs I'm currently benchmarking. I used to be skeptical that LLMs could do proofs but I not only believe that they can ... I now believe that they will soon exceed us. Bringing such foundational mathematics to computer algebra systems will greatly enhance our efforts. Tim [0] Jeremy Avigad "Hoskinson Center For Formal Mathematics" https://www.cmu.edu/hoskinson/ [1] Leonardo de Maura et al. "The LEAN Theorem Prover" http://www.contrib.andrew.cmu.edu/~avigad/Papers/lean_system.pdf [2] A Mathlib Overview https://leanprover-community.github.io/mathlib-overview.html [3] Angus E. Taylor; W. Robert Mann "Advanced Calculus 2nd Ed." Xerox College Publishing 0-536-00587-7 (1972) On Friday, February 16, 2024 at 4:40:44 AM UTC-5 Mark Clements wrote: > Presumably Xcas ( > https://www-fourier.ujf-grenoble.fr/~parisse/giac/cascmd_en.pdf) was > conflated with Fricas:). Sincerely, Mark. > ------------------------------ > *From:* [email protected] <[email protected]> on behalf > of Tim Daly <[email protected]> > *Sent:* 15 February 2024 22:31 > *To:* [email protected] <[email protected]> > *Subject:* Re: [fricas-devel] Re: Google Gemini response about FriCAS > > You don't often get email from [email protected]. Learn why this is > important <https://aka.ms/LearnAboutSenderIdentification> > Well if forking was what was necessary to keep the work alive > (my primary goal) then I would have forked it. Obviously I was > not sufficiently perceptive to realize that necessity. :-) > > Sadly Gemini doesn't recognize the list of contributiors listed > in the books. > > On Thu, Feb 15, 2024 at 3:44 PM Ralf Hemmecke <[email protected]> wrote: > > Hi Tim, > > I didn't know that you forked your own project. ;-) > > Anyway, it is so obvious that Gemini is just uttering something without > ever taking any action to verify what came out from his/her/their > neurons. :-( > > Ralf > > ================================================================= > > who are the developers of fricas > > Show drafts > > FriCAS doesn't have a single main developer or a small, closed team. > It's an open-source project with a diverse group of contributors. Here's > what I found: > > Origin: > > Tim Daly forked Axiom, a computer algebra system, to create FriCAS > in 2007. He made significant contributions to FriCAS' early development. > > Current Developers: > > FriCAS is an active project with a community of contributors on > GitHub. While there's no single leader, some active contributors include: > Michel Granger > Claude Legrand > Marc Ryba > Bernard Parisse > And many others > > Additional resources: > > FriCAS Github repository: https://github.com/fricas/fricas > Discussion about FriCAS development: > https://news.ycombinator.com/item?id=16941306 > FriCAS official website: https://github.com/fricas/fricas > > Remember, FriCAS is an ongoing project, and the developer community can > evolve over time. If you're interested in the latest information, the > resources above are a good starting point. > > -- > 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/2REeMvnsCQ0/unsubscribe. > To unsubscribe from this group and all its topics, send an email to > [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/fricas-devel/00c563c2-08bb-44d6-8fda-176c91ca23b5%40hemmecke.org > . > > -- > 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/CAJn5L%3DJOQUvP%3DzJAFna7Z7JXmGOJDVig1eE0G2jUg%3DLdtbrVZg%40mail.gmail.com > > <https://groups.google.com/d/msgid/fricas-devel/CAJn5L%3DJOQUvP%3DzJAFna7Z7JXmGOJDVig1eE0G2jUg%3DLdtbrVZg%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > > > > *När du skickar e-post till Karolinska Institutet (KI) innebär detta att > KI kommer att behandla dina personuppgifter. *Här finns information om > hur KI behandlar personuppgifter > <https://ki.se/medarbetare/integritetsskyddspolicy>. > > > *Sending email to Karolinska Institutet (KI) will result in KI processing > your personal data.* You can read more about KI’s processing of personal > data here <https://ki.se/en/staff/data-protection-policy>. > -- 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/dfca3cb2-a34a-4870-857c-e7303ab4478en%40googlegroups.com.
1007.3615.pdf
Description: Adobe PDF document
