Yes, but even more than that.
The goal is to make Axiom a "trusted system" for the whole of
computational mathematics.
To do this, consider this (not entirely random) collection of systems
and facts:
1) Trusted systems are built using the de Bruijn principle. See, for example,
https://pdfs.seman
Tim,
When I read this I am picking up a slightly different flavor than what I
got from your first message in the thread.
You first message seemed to me to be about "merging computer algebra and
proof technology" but this message seems to be about running the two in
parallel.
I really like
