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 On Friday, February 16, 2024 at 12:21:41 PM UTC-5 Tim Daly wrote: > 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/9554f7d6-b37c-4a17-9fe5-8c24e2bfd7c4n%40googlegroups.com.
