The COQ team at INRIA has released an online book called "Mathematical Components" which covers a library that simplifies proofs. This looks like an excellent match to Axiom and Latex. See, for example, slide 19 of this presentation.
ssr.msr-inria.inria.fr/doc/tutorial-itp13/slides.pdf The free book is available at https://math-comp.github.io/mcb/book.pdf for those who want to follow along on the effort to prove Axiom correct. Tim
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
