Comment by daly | Hacker News Reader

Comment by daly | Hacker News Reader

Tim Daly here...

Axiom is alive, well, and under active development. The current effort is merging the LEAN [0] proof technology with the Axiom algebra. This involves some deep restructuring. The target result is proven algorithms, something missing in current CAS work.

(Note that this is project goal F on http://axiom-developer.org)

The effort involves building a parallel architecture to the current Axiom category / domain layout to enable functions to use LEAN's axioms, definitions, and tactics to prove existing algorithms.

In addition, Axiom now uses Common Lisp CLOS to enable work using dependent types, something not currently available in the legacy system. The algebra hierarchy is now a CLOS hierarchy which enables a lot of flexible extensions.

There is no point in publishing the work as open source since it is still in the active research phase. When released it will be announced on the http://axiom-developer.org website and uploaded to github.

One of the Axiom algorithms (Groebner basis[1]) has been proven in Coq.

Wikipedia contains the literate form of Axiom[2] , including the original book restored from the NAG files.

There is an active fork maintaining the legacy code as mentioned above.

[0] The LEAN Theorem Prover https://www.andrew.cmu.edu/user/avigad/Papers/lean_system.pd...

[1] Bruno Buchberger. Bruno buchberger’s phd thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Journal of Symbolic ComputationVolume 41, Issues 3-4, Logic, Mathematics and Computer Science: Interactions in honor of Bruno Buchberger (60th birthday),, 2006.

[2] Wikipedia Axiom https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system...

Hi Tim,

So first of all thank you Axiom and all the work you have put in the system over the years. Second, the integration with LEAN seems like an amazing step forward. Is there anything on the internet I can read more about this? How would it work? Would it be beneficial for education purposes or mainly for research? Third, I am otherwise engaged in other projects these days, but a long life dream of mine is to build a CAS from scratch. That said, I wouldn't mind start collaborating with a team improving an existing one like Axiom. The "How to participate" link is just "TODO", is there any way I can get in touch with the development team?

Thanks for the "all the work" complement. Despite all, it is more fun than work.

Computer algebra algorithms are basically functions. Axiom is unique in that it organizes the functions based on a group theory scaffold. Thus you can know that certain matrices commute but rectangular ones don't. Algorithms that know how to commute live in the commutative "category" in Axiom. So the game is to distribute LEAN's commutative axioms in their proper place in the group theory inheritance scaffold so they are available when they apply.

Axiom arranges the world into "categories" (not category theory stuff) and "domains". The LEAN structure is a third structure (actually fourth but...) built in parallel so that a theorem that proves that certain matrices commute will only be available when it applies. When you try to prove your algorithm you have a collection of LEAN axioms, definitions, and tactics that are valid and apply to your particular function. If your algorithm used rectangular matrices the commutative theorems would not be visible and thus not available in a proof step. Due to the hierarchical nature, once you prove an algorithm you can also use it in other downstream proofs, for example, using proven data structures and their properties.

I have not published any papers on the subject. I'm no longer anywhere in the academic pipeline so a paper wouldn't get very far. Plus this is "in the cracks" kind of research that doesn't seem to fit into either camp.

As for the education or research question... I'm trying to do what I call "computational mathematics". It would have "real world impact" for Proof Systems so they would be able to depend on and use proven computer algebra results. Computer algebra systems would benefit by giving proven answers. Both areas would benefit.

Don't try to build a computer algebra system from scratch. Axiom has hundreds of years of PhD level research work embedded in its code. There is no way to reproduce some of it as the people have died. Researching just one of the algorithms could take the equivalent of a PhD effort. I tried to introduce literate programming so that people could learn to maintain, modify, and extend Axiom. The idea is that you could "read the docs" and both learn from the authors and have embedded pointers to the theory literature. Without literate programming I believe that the whole effort will eventually die as the learning curve is very steep. Literate programming was an attempt to keep Axiom "alive". Nobody wanted it. I gave a talk on it once: https://www.youtube.com/watch?v=Av0PQDVTP4A&ab_channel=NextD...

There is no "team". There is just me. Apparently I'm bad at "team". I have no desire to get forked again.

Thanks for the invaluable feedback! Looking forward to see the day Axiom and LEAN are integrated together. Good luck!

Hi Tim,

>There is no point in publishing the work as open source since it is still in the active research phase.

That sounds very interesting to me at least, I'd appreciate being able to take a peek.

Having experience with prior open source work I'm not likely to release the current effort until I'm much closer to completion. The whole idea of CAS and Proof has already generated a hostile reception from both areas in my email stream.

I've already proven that if I did release Axiom again I'm too socially inept to manage the process anyway. I'd release a technical paper or two but I'm no longer associated with CMU so I'm pretty much a "hobby researcher" I guess. The last Axiom presentation was the invited talk at Notre Dame prior to Covid.

There are a lot of interesting things "in the works" though. One is the idea of "proof down to the metal" (aka Proof Carrying Code[0]). The use of (FPGA) field programmable gate arrays[1] and the RISC-V[2] architecture soft-implemented in the FPGA means that I can run the LEAN proof in parallel with the algorithm at the hardware level. This not only proves the algorithm correct, it proves the implementation correct. I have a few FPGAs.

It's all fun and games but I have to wait to release it.

[0] https://en.wikipedia.org/wiki/Proof-carrying_code

[1] https://en.wikipedia.org/wiki/Field-programmable_gate_array

[2] https://en.wikipedia.org/wiki/RISC-V

Im not in this field so this might not be a good question, but why integration with LEAN and not ACL2, which is already written in Common Lisp

I worked with Nqthm and ACL2. They seem best adapted to hardware verification.

LEAN is pushing the edge of undergrad mathematics.

"Faszinating" that a lot of these systems seem to be implemented from scratch in object-oriented C++ (?), instead of Prolog, SML, OCAML, Haskell, Lisp, ... what went wrong?

Thanks, I wasnt aware of the differences between various provers.

Reply on news.ycombinator.com