What an interesting history -- thanks for sharing it! Please do not be too hard on yourself -- keping open source software alive is tough.
Regarding proofs, the lisp (and gcl) based ACL2 is probably the easiest to integrate, as you are aware given the stubs in the Makefiles. But of course this is a huge project. Take care, Tim Daly <axiom...@gmail.com> writes: > There was never any deep interest in Axiom at CCNY. > > I got the CD from NAG just a few months before the CCNY offer. > I had a written agreement with CCNY when I took the job that > I would not work on Axiom during working hours or on CCNY > equipment if they agreed to make no claim on Axiom. I did this > so Axiom could remain free and open source. > > My job involved building Magnus which was an Infinite Group > Theory platform. I had many conversations with Gilbert about > putting some of the Magnus algorithms in Axiom. > > Eventually Gilbert wanted me to created a research proposal we > could submit for funding. This was important because CCNY only > paid salaries during the school year. Salaries during the summer > came from research grants. > > I wrote a research grant for "Indefinite Integers", the idea being the > ability to declare a variable as an Integer but never specify the value. > Thus there might be polynomials with Indefinite Integer coefficients. > I had been working on the idea and algorithms at home as part of Axiom. > > The great benefit of this agreement is that it gave me time to build > a self-hosting version of Axiom. The version I used needed an Axiom > image from NAG which I could use but not distribute. The problem > was rather difficult and took a lot of work to untangle the algebra > and find the essential kernel. Once that was solved I released > a self-hosted Axiom that would build from sources. > > Gilbert suggested I spend some of my time working on Axiom as part of the > grant and that he would make no claims on Axiom. That grant funded > several researchers over the summer. I made some progress on the > idea but pressure was on to develop Magnus. This resulted in an > attempted merger of Magnus algorithms into Axiom, work that was > lost when I left CCNY. > > It also resulted in the Doyen "Computational Mathematics platform" > that was distributed on the CD at the conference. Doyen was very > similar in spirit to SageMath but William Stein did a much better job > and is clearly a much better leader and researcher than I am. > > Gilbert wanted to showcase the Axiom work so I created and hosted > the Axiom conference. That conference was attended by a person from > CMU which led to a job offer at CMU which I accepted. I brought Magnus > up to speed before I left and I have many copies of the Magnus CD I > distributed at CMU. > > A similar agreement for Axiom independence was reached with CMU > so all of the development was on my free time and my own equipment. > The CMU job involved reverse-engineering malware so there was no > conflict and no interest in Axiom. I took a follow-on job with Scott Fahlman > to develop a human/robot system to change a car tire, again with no > conflict with Axiom. > > Years later after I left CMU I was working on merging Axiom and proofs. > > I called Jeremy Avigad, a CMU professor in Math and Philosophy to ask > him for help with struggles I had about program proofs. Jeremy invited me > to audit his course. I made a presentation of Axiom to the head of the > computer science department, Frank Pfenning and several other > professors. Frank offered me an unpaid "visiting scholar" position which > lasted > 6 years. I audited about a dozen courses and made great progress on > merging Axiom and Lean, CMU's proof system, presented at Notre Dame. > I dearly miss the visiting scholar position and especially the library access. > > My focus on research and lack of management skills eventually killed Axiom. > > Tim > > On Thu, May 8, 2025 at 9:18 AM Camm Maguire <c...@maguirefamily.org> wrote: > > Greetings! > > Tim Daly <axiom...@gmail.com> writes: > > > I created a "Computational Science Platform" CD at CCNY that > > was a bootable CD containing Axiom and Doyen. Doyen was > > my first attempt at a "computational mathematics platform". > > It was distributed at the Axiom conference I hosted at CCNY. > > The copies likely no longer exist except on my shelf. > > I think I was at this one! Who knows I may have the only external copy > somewhere on my shelf :-). > > Is there any remaining interest or support for AXIOM at CCNY? > > Take care, > -- > Camm Maguire c...@maguirefamily.org > ========================================================================== > "The earth is but one country, and mankind its citizens." -- Baha'u'llah > -- Camm Maguire c...@maguirefamily.org ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah
