I have an active discussion on Zulip / Lean (the general/syntax thread) The issue is "long term stability".
Axiom code from the last century still compiles and gives the same answers. Latex code from the last century still compiles and gives the same document. I need to be able to write Definitions, Lemmas, and a Proof that will machine check correctly at the "30 year horizon". It does me no good to use Lean to prove Axiom's GCD algorithm if the proof fails next week. Lisp had this problem and it was essentially solved with a standards effort to create common lisp. It does me no good to have a proof system where the tactics can change, the syntax can change, and the kernel is unstable. I can't do long-term, "30 year horizon" computational mathematics on that basis. I think someone should raise the "common core proof standard effort" so that all of the systems could import / export "raw" proofs (at a minimum). Or at least a common core for systems using equivalent logic rules. It is reasonable to assume that a "proof" is a long-lived object and that computational mathematical results are "stable". Competing on "features" is for game programmers, not mathematicians. Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
