When Axiom Sane is paired with a proof checker (e.g. with Lean)
there is a certain amount of verification that is involved.
Axiom will provide proofs (presumably validated by Lean) for its
algorithms. Ideally, when a computation is requested from Lean
for a GCD, the result as well as a proof of th
Provisos that is, 'formula SUCH pre/post-conditions'
A computer algebra system ought to know and ought to provide
information about the domain and range of a resulting formula.
I've been pushing this effort since the 1980s (hence the
SuchThat domain).
It turns out that computing with, carryin
