William, > the hurdle for newcomers to learn it would be quite a challenge.
The point of the literate programming effort was to capture the expertise for future developers. The question was how to keep Axiom alive once the core developers (e.g. Bronstein) are no longer available to answer questions. The ideal case would be to give the literate sources to someone and they would be able to maintain and extend the code. Since the system is built from the literate documents they would always be up to date. > Any chance that Axiom may be discovered by the AI community? I built a machine with a GPU board, downloaded and ran 71 LLMs to rank them on their ability to "Prove the greatest common divisor theorem". The game was to find the LLMs that were best suited for the proof task. Proofs share a lot of characteristics of games. They have a state space, they have a limited number of actions (tactics), they have intermediate metrics (substeps solved), and they have a well-defined goal state. All of these characteristics make reinforcement learning for proofs using the Bellman equation an ideal case. The Axiom game was to construct the Category-Domain-Proof hierarchy so that within the Proof inheritance chain there would be an "LLM function" that would assist in proving Axiom's algorithms. With the latest open source Deepseek-R1 this is probably possible. Unfortunately I don't have the resources to run the larger models. My home office is already 10F degrees above the rest of the house :-) The largest model I tried ran for 28 days. Another issue is that Axiom's Proof hierarchy has embedded definitions but the LLMs don't know how to use them. The necessary but unavailable step is self-modifying systems so that the definitions can be used without unfolding them all the way down to the primitives. Hopefully test-time training will allow this but again I don't have the resources to try this. I looked into creating a modified Word2Vec table with "math words" but then I'd have to train a new fundamental model which is again a resource issue for me. There is so much research still to be done. Where are the graduate students when you need them? :-) Hope things are well with you. Tim On Wed, Feb 5, 2025 at 2:52 PM William Sit <w...@ccny.cuny.edu> wrote: > Dear Tim and Camm: > Sorry to hear the loss of accessibility to Axiom. These days, it is > difficult to keep up with even ordinary computing needs, and impossible to > give attention to technical projects. You both have dedicated for decades > to maintaining and improving Axiom. Somehow, Axiom might be "rediscovered", > but the hurdle for newcomers to learn it would be quite a challenge. > We need to feel satisfied in having contributed to progress in computer > algebra and at our age, relax and let the fate of Axiom fall wherever it > may. Nonetheless, I am still optimistic. > Any chance that Axiom may be discovered by the AI community? I tested > Copilot (by MIcrosoft) on a simple math question and it gave me a wrong > answer (with a detailed wrong proof), although it accepted my correction. > The question was: Is the inverse of an order-preserving bijection between > two partially ordered sets also order-preserving? Would Axiom be useful to > provide a correct answer (which is "no", and give a counter example)? > > Regards, > William > ------------------------------ > *From:* axiom-developer-bounces+wyscc=sci.ccny.cuny....@nongnu.org > <axiom-developer-bounces+wyscc=sci.ccny.cuny....@nongnu.org> on behalf of > Tim Daly <axiom...@gmail.com> > *Sent:* Wednesday, February 5, 2025 2:16 PM > *To:* Camm Maguire <c...@maguirefamily.org>; Tim Daly <axiom...@gmail.com> > *Cc:* axiom-dev <axiom-develo...@nongnu.org>; Barry Trager < > bmtra...@gmail.com>; Ralf Hemmecke <r...@hemmecke.org>; Waldek Hebisch < > hebi...@math.uni.wroc.pl>; fricas-devel@googlegroups.com < > fricas-devel@googlegroups.com> > *Subject:* [EXTERNAL] Re: Project website > > Axiom is dead. The site got no traffic. I don't have github access anymore > due to Microsoft's multi-factor "protection". It was a good 24 years. > > It was fun while it lasted. The last effort was a new parallel construction > of "Category, Domain, Proof" which integrated LEAN proofs (e.g. about > Abelians) > as a separate, connected hierarchy, enabling proofs of algorithms like the > GCD. > That will never see the light of day. > > The real cause of death is my lack of management skills and objectionable > personality. > I thought the point of research software was to innovate, not polish. > Nobody agreed. > Adding proofs and being literate were too radical. Dick Jenks would have > succeeded. > > My real frustration is that the several hundred people who contributed in > large and > small ways over many years don't seem to even get mentioned. Credit is so > easy > to share. Axiom would never have been re-created without effort from > people like you. > At least I personally say "Thank you, Camm." > > Tim > > > > > On Wed, Feb 5, 2025 at 12:50 PM Camm Maguire <c...@maguirefamily.org> > wrote: > > Hi Tim! I hope this note finds you well! > > Just noticing that axiom-developer.org > <https://urldefense.proofpoint.com/v2/url?u=http-3A__axiom-2Ddeveloper.org&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc&m=OkUyTzbIV4R1aMIbDzp1OwwzZPKdeuGxSnzQkyRX8VWOsYitar-IiPReXO2cdhz4&s=R_yEGjorI_RgWgBaU-UVSbeQbPQM9IR6ZVtYEineLbM&e=> > appears to be inaccessible. > Github appears more recent. What is the best way to keep current with > axiom? > > Take care, > -- > Camm Maguire c...@maguirefamily.org > ========================================================================== > "The earth is but one country, and mankind its citizens." -- Baha'u'llah > > -- 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 visit https://groups.google.com/d/msgid/fricas-devel/CAJn5L%3DLRF04-AP9E%3Dqkzdmt8h_bx0HFp8NupxfE%3DP-Ft2iDWxw%40mail.gmail.com.
