Re: [fricas-devel] Re: Google Gemini response about FriCAS
ting 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:* fricas...@googlegroups.com on >> behalf of Tim Daly >> *Sent:* 15 February 2024 22:31 >> *To:* fricas...@googlegroups.com >> *Subject:* Re: [fricas-devel] Re: Google Gemini response about FriCAS >> >> You don't often get email from axio...@gmail.com. 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 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 developme
Re: [fricas-devel] Re: Google Gemini response about FriCAS
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:* fricas...@googlegroups.com on behalf > of Tim Daly > *Sent:* 15 February 2024 22:31 > *To:* fricas...@googlegroups.com > *Subject:* Re: [fricas-devel] Re: Google Gemini response about FriCAS > > You don't often get email from axio...@gmail.com. Learn why this is > important <https://aka.ms/LearnAboutSenderIdentification> > Wel
Re: [fricas-devel] Re: Google Gemini response about FriCAS
Presumably Xcas (https://www-fourier.ujf-grenoble.fr/~parisse/giac/cascmd_en.pdf) was conflated with Fricas:). Sincerely, Mark. From: fricas-devel@googlegroups.com on behalf of Tim Daly Sent: 15 February 2024 22:31 To: fricas-devel@googlegroups.com Subject: Re: [fricas-devel] Re: Google Gemini response about FriCAS You don't often get email from axiom...@gmail.com. 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 mailto:r...@hemmecke.org>> 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 fricas-devel+unsubscr...@googlegroups.com<mailto:fricas-devel%2bunsubscr...@googlegroups.com>. 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 fricas-devel+unsubscr...@googlegroups.com<mailto:fricas-devel+unsubscr...@googlegroups.com>. 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_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 fricas-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/MM0P280MB000894B753609268836209C9F04C2%40MM0P280MB0008.SWEP280.PROD.OUTLOOK.COM.
Re: [fricas-devel] Re: Google Gemini response about FriCAS
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 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 > fricas-devel+unsubscr...@googlegroups.com. > 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 fricas-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/CAJn5L%3DJOQUvP%3DzJAFna7Z7JXmGOJDVig1eE0G2jUg%3DLdtbrVZg%40mail.gmail.com.
Re: [fricas-devel] Re: Google Gemini response about FriCAS
On 2/15/24 21:48, Dima Pasechnik wrote: Oh, wow, Bernard Parisse develops FriCAS while taking a break from developing giac... Yes, we capture all eventually ;-) ... you only must ask Gemini long enough. Ralf -- 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/1f09d2f1-94c3-4246-9916-a0c2499ca680%40hemmecke.org.
Re: [fricas-devel] Re: Google Gemini response about FriCAS
Oh, wow, Bernard Parisse develops FriCAS while taking a break from developing giac... On 15 February 2024 20:44:05 GMT, Ralf Hemmecke 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 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/4836A184-F010-4C08-8C1B-93BCFED9A152%40gmail.com.
Re: [fricas-devel] Re: Google Gemini response about FriCAS
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 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/00c563c2-08bb-44d6-8fda-176c91ca23b5%40hemmecke.org.
Re: [fricas-devel] Re: Google Gemini response about FriCAS
The answer to the question below is very accurate. ;-) Maybe I should be looking for Claude Leloutre at Linz. Perhaps he is the one that maintains the Mercurial repository of FriCAS. I am now very convinced that AI is the future. ;-) Ralf === who are the developers of fricas Show drafts While FriCAS doesn't have a single central development team, its development has been driven by the contributions of numerous individuals over many years. Here's what I found: Origins: FriCAS started as a fork of Axiom (another CAS) by Renaud Dupont in 2007. Initially, he aimed for a smaller and cleaner codebase than Axiom. Early development continued with contributions from Bernard Parisse, Claude Leloutre, and others. Present Day: Since then, development has become more decentralized, with contributions coming from researchers, mathematicians, and programmers around the world. The project utilizes a Mercurial repository (similar to Git) hosted on SourceForge, where you can find a list of committers and contributors. Some notable contributors currently include Claude Leloutre, Johannes Kepler University Linz, and University of Paris. Additional Resources: You can find the list of committers and contributors on the FriCAS source code repository: https://sourceforge.net/projects/fricas/ The FriCAS website mentions some key developers: https://fricas.sourceforge.net/ It's important to note that FriCAS benefits from the collaborative efforts of a diverse community, not just a single team. This decentralized approach fosters ongoing development and keeps the system relevant and updated. -- 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/efaa4f09-50b6-48d5-a581-ba6562288c69%40hemmecke.org.
[fricas-devel] Re: Google Gemini response about FriCAS
Scroll down. I have no idea why there is so much whitespace On Thursday, February 15, 2024 at 1:39:37 PM UTC-5 Tim Daly wrote: > Tell me about the Fricas computer algebra system > Show drafts > > FriCAS is another interesting open-source computer algebra system with > some similarities to Axiom, but also distinct features and strengths. > Here's what you need to know: > > *History:* > >- Forked from Axiom in 2007 with the goal of creating a more modern >and user-friendly system. >- Actively developed by a small but dedicated community. >- Emphasis on open collaboration and lightweight development >methodology. > > *Features:* > >- *General-purpose:* Similar to Axiom, handles various mathematical >tasks like symbolic calculations, integration, differentiation, and >more. >- *Strongly typed:* Similar to Axiom, uses a strict type system for >accuracy and clarity. >- *SPAD programming language:* Similar syntax to Axiom's Lisp, but >aims for simplicity and readability. >- *Multiple interfaces:* Can be used through a command line, various >graphical interfaces, and even integrates with Jupyter notebooks. >- *Growing library:* Offers a large and diverse library of functions >and packages for various domains. > > *Applications:* > >- Similar to Axiom, applicable in research, education, engineering, >and scientific fields for symbolic manipulation and complex mathematical >tasks. > > *Strengths:* > >- User-friendly interface options compared to Axiom. >- Lightweight and portable, easily runs on various platforms. >- Actively developed with new features and improvements often added. >- Open-source and community-driven, accessible to anyone. > > *Weaknesses:* > >- Less mature and comprehensive than Axiom, especially in advanced >areas. >- Community might be smaller than Axiom, leading to fewer resources >and support options. >- Development pace can be slower compared to commercially backed >systems. > > *Overall:* > > FriCAS is a user-friendly and actively developed open-source computer > algebra system suitable for various mathematical tasks. While it may not > be as comprehensive as Axiom for highly specialized needs, it offers a > good balance of functionality and ease of use. If you're looking for a > user-friendly open-source option for your mathematical work, FriCAS is > worth considering. > > Here are some resources to learn more: > >- *FriCAS website:* [[invalid URL removed]]([invalid URL removed]) >- *FriCAS documentation:* https://fricas.github.io/ >- *FriCAS GitHub repository:* https://github.com/fricas/fricas > > I hope this helps you to further explore the capabilities of FriCAS! > -- 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/faff8af4-53fc-4f7c-a351-84af3efaea82n%40googlegroups.com.
