Google Gemini response about FriCAS

[Tim Daly]

Tell me about the Fricas computer algebra system

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!

[Tim Daly]

Scroll down. I have no idea why there is so much whitespace

[Ralf Hemmecke]

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.

[Ralf Hemmecke]

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.

[Dima Pasechnik]

Oh, wow, Bernard Parisse develops FriCAS while taking a break from developing giac...

[Ralf Hemmecke]

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

[Tim Daly]

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.

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

[Mark Clements]

Presumably Xcas (https://www-fourier.ujf-grenoble.fr/~parisse/giac/cascmd_en.pdf) was conflated with Fricas:). Sincerely, Mark.

---

From: fricas...@googlegroups.com <fricas...@googlegroups.com> on behalf of Tim Daly <axio...@gmail.com>
Sent: 15 February 2024 22:31
To: fricas...@googlegroups.com <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

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/CAJn5L%3DJOQUvP%3DzJAFna7Z7JXmGOJDVig1eE0G2jUg%3DLdtbrVZg%40mail.gmail.com.

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. 

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. 

[Tim Daly]

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)

[Tim Daly]

Just so you know, Axiom is the work of a LOT of people.

FriCAS should update this list. Credit is important.

Roy Adler                Christian Aistleitner    Michael Albaugh
Cyril Alberga            Jason Allen              Richard Anderson
George Andrews           Jerry Archibald          S.J. Atkins
Jeremy Avigad            Brent Baccala            Knut Bahr
Henry Baker              Martin Baker             Stephen Balzac
Yurij Baransky           David R. Barton          Thomas Baruchel
Gerald Baumgartner       Gilbert Baumslag         Michael Becker
Nelson H. F. Beebe       Jay Belanger             Siddharth Bhat
David Bindel             Fred Blair               Vladimir Bondarenko
Ed Borasky               Mark Botch               Raoul Bourquin
Alexandre Bouyer         Karen Braman             Wolfgang Brehm
Peter A. Broadbery       Martin Brock             Manuel Bronstein
Christopher Brown        Stephen Buchwald         Florian Bundschuh
Luanne Burns             William Burge            Ralph Byers
Quentin Carpent          Jacques Carette          Pierre Casteran
Robert Cavines           Pablo Cayuela            Bruce Char
Ondrej Certik            Tzu-Yi Chen              Bobby Cheng
Cheekai Chin             David V. Chudnovsky      Gregory V. Chudnovsky
Mark Clements            Roland Coeurjoly         Emil Cohen
Hirsh Cohen              Josh Cohen               James Cloos
Jia Zhao Cong            Christophe Conil         Don Coppersmith
George Corliss           Robert Corless           Gary Cornell
Frank Costa              Meino Cramer             Karl Crary
Jeremy Du Croz           David Cyganski           Nathaniel Daly
Timothy Daly Sr.         Timothy Daly Jr.         James H. Davenport
David Day                James Demmel             Didier Deshommes
Michael Dewar            Inderjit Dhillon         Jack Dongarra
Jean Della Dora          Gabriel Dos Reis         Claire DiCrescendo
Sam Dooley               Pierre Doucy             Nicolas James Doye
Zlatko Drmac             Lionel Ducos             Iain Duff
Lee Duhem                Martin Dunstan           Brian Dupee
Dominique Duval          Robert Edwards           Hans-Dieter Ehrich
Heow Eide-Goodman        Alexandra Elbakyan       Carl Engelman
Lars Erickson            Mark Fahey               William Farmer
Richard Fateman          Bertfried Fauser         Stuart Feldman
John Fletcher            Brian Ford               Albrecht Fortenbacher
George Frances           Constantine Frangos      Timothy Freeman
Korrinn Fu               Marc Gaetano             Rudiger Gebauer
Van de Geijn             Kathy Gerber             Patricia Gianni
Eitan Gurari             Gustavo Goertkin         Samantha Goldrich
Max Goldstein            Holger Gollan            Teresa Gomez-Diaz
Ralph Gomory             Laureano Gonzalez-Vega   Stephen Gortler
Johannes Grabmeier       Matt Grayson             Martin Griss
Andrey G. Grozin         Klaus Ebbe Grue          James Griesmer
Vladimir Grinberg        Oswald Gschnitzer        Ming Gu
Fred Gustavson           Jocelyn Guidry           Gaetan Hache
Steve Hague              Satoshi Hamaguchi        Sven Hammarling
Mike Hansen              Richard Hanson           Richard Harke
Joseph Harry             Bill Hart                Vilya Harvey
Martin Hassner           Arthur S. Hathaway       Dan Hatton
Waldek Hebisch           Karl Hegbloom            Ralf Hemmecke
Tony Hearn               Henderson                Antoine Hersen
Nicholas J. Higham       Lou Hodes                Alan Hoffman
Hoon Hong                Roger House              Joris van der Hoeven
Gernot Hueber            Pietro Iglio             Joan Jaffe
Alejandro Jakubi         Richard Jenks            Bo Kagstrom
William Kahan            Kyriakos Kalorkoti       Kai Kaminski
Matt Kaufmann            Grant Keady              Tom Kelsey
Wilfrid Kendall          Tony Kennedy             David Kincaid
Keshav Kini              Knut Korsvold            Ted Kosan
Paul Kosinski            Igor Kozachenko          Fred Krogh
Klaus Kusche             Bernhard Kutzler         Tim Lahey
Larry Lambe              Magnus Larsson           Kaj Laurson
Charles Lawson           George L. Legendre       Franz Lehner
Frederic Lehobey         Michel Levaud            Howard Levy
J. Lewis                 Ren-Cang Li              Xin Li
John Lipson              Rudiger Loos             Craig Lucas
Michael Lucks            Richard Luczak           Camm Maguire
Dave Mainey              Francois Maltey          William Martin
Ursula Martin            Dan Martins              Osni Marques
Alasdair McAndrew        Bob McElrath             Michael McGettrick
Roland McGrath           Paul McJones             Bob McNeill
Edi Meier                Ian Meikle               David Mentre
Simon Michael            Jonathan Millen          Victor S. Miller
Gerard Milmeister        William Miranker         Mohammed Mobarak
H. Michael Moeller       Michael Monagan          Marc Moreno-Maza
Scott Morrison           Joel Moses               Mark Murray
William Naylor           Patrice Naudin           C. Andrew Neff
John Nelder              Godfrey Nolan            Arthur Norman
Jinzhong Niu             Michael O'Connor         Summat Oemrawsingh
Kostas Oikonomou         Humberto Ortiz-Zuazaga   Julian A. Padget
Bill Page                David Parnas             Igor Pashev
Norm Pass                Susan Pelzel             Michel Petitot
Didier Pinchon           Ayal Pinkus              Frederick H. Pitts
Frank Pfenning           Erik Poll                Jose Alfredo Portes
E. Quintana-Orti         Gregorio Quintana-Orti   Beresford Parlett
A. Petitet               Andre Platzer            Peter Poromaas
Greg Puhak               Claude Quitte            Arthur C. Ralfs
Norman Ramsey            Anatoly Raportirenko     Guilherme Reis
Huan Ren                 Albert D. Rich           Michael Richardson
Jason Riedy              Renaud Rioboo            Robert Risch
Wilken Rivera            Jean Rivlin              Nicolas Robidoux
Simon Robinson           Raymond Rogers           Michael Rothstein
Martin Rubey             Jeff Rutter              R.W Ryniker II
Philip Santas            Grigory Sarnitskiy       David Saunders
Aleksej Saushev          Alfred Scheerhorn        William Schelter
Gerhard Schneider        Martin Schoenert         Marshall Schor
Frithjof Schulze         Fritz Schwartz           Jens Axel Segaard
Steven Segletes          Srinivasan Seshan        V. Sima
Nick Simicich            Peter Simons             William Sit
Elena Smirnova           Jacob Nyffeler Smith     Matthieu Sozeau
Richard Stallman         Ken Stanley              William Stein
Jonathan Steinbach       Alexander Stepanov       Doug Stewart
Fabio Stumbo             Christine Sundaresan     Ben Collins-Sussman
Klaus Sutner             Robert Sutor             Moss E. Sweedler
Eugene Surowitz          Yong Kiam Tan            Max Tegmark
T. Doug Telford          James Thatcher           Laurent Thery
Balbir Thomas            Mike Thomas              Carol Thompson
Simon Thompson           Dylan Thurston           Francoise Tisseur
Steve Toleque            Dick Toupin              Raymond Toy
Barry Trager             Hale Trotter             Themos T. Tsikas
Gregory Vanuxem          Kresimir Veselic         Christof Voemel
E.G. Wagner              Bernhard Wall            Justin Walker
Paul Wang                Stephen Watt             Andreas Weber
Jaap Weel                Al Weis                  Juergen Weiss
M. Weller                Mark Wegman              James Wen
Thorsten Werther         Michael Wester           R. Clint Whaley
James T. Wheeler         John M. Wiley            Berhard Will
Clifton J. Williamson    Stephen Wilson           Shmuel Winograd
Robert Wisbauer          Sandra Wityak            Waldemar Wiwianka
Knut Wolf                Hans Peter Wuermli       Yanyang Xiao
Liu Xiaojun              Clifford Yapp            David Yun
Qian Yun                 Vadim Zhytnikov          Paul Zimmermann
Richard Zippel           Wolfgang Zocher          Evelyn Zoernack
Bruno Zuercher           Dan Zwillinger