Very good points. It helps to list the requirements of a system before you actually build it! I did something very similar when I wrote about what I would like to see in an interactive theorem proving (ITP) system: https://doi.org/10.47757/practal.1

This worked out great so far in that I managed to come up with a logic which I believe is actually the BEST logic for mathematics, Abstraction Logic (AL): https://doi.org/10.47757/pal.2

Furthermore, I think the ideal ITP system and the ideal Computer Algebra System (CAS) are actually the same thing. Many will dispute that, but this is just because they cannot look further than the shortcomings of current incarnations of both concepts. I actually think that AL will help to unify those two concepts, as an AL term is a very simple thing, and much easier to manipulate than a typed term of some complicated type theory!

A lot of the points you list are really just saying that you want your CAS to be an ITP system: a) Inert expressions b) Based on math c) Based on typed math d) Type-integrated symbolics and enclosures e) Good for Inequalities g) Large but lean h) Text-friendly (and human-friendly)

Your other points are points that people want for ITP systems, too: i) Integers j) Good math display k) Well-named

As for types, I believe now that a static type system just does not cut it. I believe something like Practical Types (which led me to AL) is the right way to go, such that you have semantic types, which are basically like sets, without requiring that everything is a set: https://doi.org/10.47757/practical.types.1

> For example, 6 has an additive inverse in ℤ but not in ℕ [...] (this is the reason why int often makes more sense than unsigned int in C, even when you have an unsigned value)

`unsigned int` isn't actually ℕ though, it's ℤ∕nℤ [1], i.e., the integers modulo n, which does have an additive inverse of 6 (being n−6).

The reason `int` often makes more sense is because it's a useful property that the additive inverse of 6 actually be less than 6 -- or more generally, that `int` isn't modular.

Agree with the overall point though, that 6 is an element of many "types". Of the CAS-adjacent languages I'm experienced with, TLA+ gets this right; SMTLIBv2 does not.

[1] https://en.wikipedia.org/wiki/Modular_arithmetic#Integers_mo...

I don't think modulo arithmetic per se includes any notion of "less". Typical definitions of "order" for an algebraic structure would require the order to be translation invariant, which isn't true in modulo arithmetic.

Fair point! I mean "less" in the same sense that "less" is defined for unsigned/modular arithmetic in most languages (e.g. C).

Wow, look at hackernews getting relevant again. nice work. great post.

> Pretty much the only systems that more or less get math right are the mathematical libraries for proof assistants (Lean, Coq, etc.). The mathematical structures and interfaces in Lean's MathLib are actually pretty close to what I'd like to see in a CAS.

This comes with HUGE practical disadvantages. Yes, it would be possible to use type theory to make a mathematically rigorous CAS, but it would never be practical. Anyone who has ever tried knows that even proving something trivial like a+b+c+d=d+b+c+a in a theorem prover requires a suprising amount of ingenuity. There are few people in the world who have the skills to define and prove something more advanced like Buchberger's algorithm, and a task like that would probably require several math papers worth of new research just to produce the slowest implementation known to mankind. And it would take years.

Author here. I'm only talking about using formalizable and mathematically consistent type definitions in a CAS, not requiring formal proofs in the implementations of types.

For example, if you want to prove a+b+c+d=d+b+c+a, you will define a, b, c, d as elements of a type R implementing the "additive abelian group" interface (or an extension of this interface, like "ring"); R = integers, for example. The CAS can then use builtin techniques for abelian additive groups to prove the property efficiently. It will not have to prove those properties from first principles.

In the distant future there could perhaps be some kind of convergence between CASes and proof assistants to completely rule out implementation errors, but this would require breakthroughs in proof automation for the reason you mentioned.

It's pretty easy in Lean/mathlib:

  import tactic
  
  example (R : Type*) [comm_ring R] (a b c d : R) :
    a + b + c + d = d + b + c + a :=
  by ring

It takes about 50ms to parse, process, and type check this example, with the ring tactic running using some VM-compiled Lean code (in Lean 4, tactics will be compiled to native code).

The way the ring tactic works is that it puts both sides of the equality into some kind of normal form, and hopefully the normal forms are the same. And, honestly, even without the ring tactic, it's easy to use just the simplifier for this if you know the incantation: simp [add_assoc, add_left_comm, add_comm]. (The simplifier is not a simple piece of software, but it's built-in and it's able to run a rewrite system while being able to normalize things when the rewrites enter loops.)

To write CAS-like tactics, in principle "all you have to do" is write algorithms that simultaneously operate on expressions and construct proofs that the expressions represent what you need them to represent.

One example of this in mathlib is the norm_num tactic, which is supposed to take expressions involving numbers, operators, and other functions, then evaluate everything as far as possible. It's something like Mathematica's evaluator, though it only evaluates using rules specifically developed for norm_num. It turns out that norm_num, even though it is operating on expressions and constructing proofs the whole way, tends to be much faster than using kernel reductions (the gold standard for correctness). That's because it's able to use faster algorithms for various functions rather than the mathematically pristine ones, for example it does multiplication using a base-2 representation of a natural number rather than in terms of its unary representation, which is the definition for the natural numbers as an inductive type.

In fact, by using these sorts of tactics it's possible to calculate things that the kernel can't calculate itself. Here are some examples using top-level commands to invoke kernel reduction and the norm_num tactic:

  #reduce 1000000 * 1000000
  -- deep recursion was detected
  
  #norm_num 1000000 * 1000000
  -- 1000000000000

(This is something that lets you use Lean as a calculator with a "repl".)

Lean also has #eval to VM-compile an expression and evaluate it there, but what's interesting about #norm_num is that while evaluating it's also constructed a proof that the answer is correct. The VM compiler and VM are considered to be untrusted code, and they certainly have not been proved to be correct in any way.

Similar story in Isabelle/HOL - no special tactics required for this example:

  lemma
    fixes a :: "'a::comm_ring"
    shows "a + b + c + d = d + b + c + a"
    by fastforce

Just for fun, I wrote up an equivalent but completely manual proof where every proof step consist of just one application of an existing fact - this is extremely verbose, but still quite short for this example:

  lemma
    fixes a :: "'a::comm_ring"
    shows "a + b + c + d = d + b + c + a"
  proof -
    note assoc = ab_semigroup_add_class.add_ac(1)
  
    have "a + b + c + d = a + (b + c + d)"
      unfolding assoc[of a] by rule
  
    also have "… = a + (d + (b + c))"
      unfolding add.commute[of d "b + c"] by rule
  
    also have "… = d + (b + c) + a"
      unfolding add.commute[of a "d + (b + c)"] by rule
  
    also have "… = d + b + c + a"
      unfolding assoc by rule
  
    finally show ?thesis .
  qed

Here's a verbose Lean calc proof using single rewrites:

  import tactic
  
  example (R : Type*) [comm_ring R] (a b c d : R) :
    a + b + c + d = d + b + c + a :=
  calc a + b + c + d = a + b + (c + d)   : by rw add_assoc
                 ... = a + (b + (c + d)) : by rw add_assoc
                 ... = b + (c + d) + a   : by rw add_comm
                 ... = c + d + b + a     : by rw add_comm b
                 ... = d + c + b + a     : by rw add_comm c
                 ... = d + (c + b) + a   : by rw add_assoc d
                 ... = d + (b + c) + a   : by rw add_comm c
                 ... = d + b + c + a     : by rw ← add_assoc

(I didn't put any thought into trying to make it be efficient.)

We are currently evaluating SymPy in Jupyter Notebooks as tool for teaching and from that experience I would add both simplicity for beginners as well as explicitness to the laundry list. Python and SymPy for example will simplify things they think is "trivial" (not so simple for teaching basics). Yet while you can be very explicit to counter such behavior, this will take away the simplicity.

> The programming language of a CAS should have a type system suitable for doing mathematics.

I find it hard to understand what type theorists are actually ever talking about because their terminology is too hard to understand (like "intuitionistic type theory" "calculus of constructions" etc).

But looking at practical PL type systems, it's always seemed like they aren't that useful for math.

- for basic engineering math you'd want units like inch vs. centimeter that just add properly, or inch vs square inch that don't add together, but it doesn't seem like those are easy to model with types.

- more abstractly, how do you use types to prove that a matrix multiplication is correct? What even is the type of an intermediate term in a matrix multiplication?

- what’s the type backing a number? Is it a bignum? But now addition is O(n) not O(1) which actually adds a lot of security issues.

Thanks for writing this! It's interesting and useful to me. I've been thinking about a personal "math helper". My context is that I have an engineering background and am currently studying physics.

Your "inert expressions" point really resonated. I'd like for my helper not to do anything to expressions I'm working with, at least initially. I want to micromanage and literally tell it what operations to do. I just want to remove the typos and -1/+1 etcetera mistakes that I tend to make. I also tend to get a bit lost in just simple algebra, so I'd like to be able to massage an expression multiple ways and keep ones that are making progress.

Have you looked at Axiom?

https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system...

> A CAS worth its name ought to be able to represent structures like transcendental number fields, rings of holomorphic functions, differential fields, transseries, and so on.

Doing this in a principled way requires implementing constructive analysis, which is not easy. Even something as simple as equality of real numbers is not constructively defined, one has to work with constructive apartness relations instead.

No. Constructive analysis is not needed for this. Classical mathematics will do just fine. Stating nonsense like this is what gives constructivism a bad name. That's not saying that there is no room for constructivism in an ideal ITP/CAS system, there certainly is!

Why would it be illegitimate? Is Zeta(-1) more or less illegitimate?

Any finite value when multiplied by zero, results in zero - unlike any other multiplication with real numbers it is a lossy operation and cannot be reversed.

Taking division as an anti-function of multiplication, 0/0 could mean any value - positive, negative, finite, infinite, infinitessimal or zero itself.

For all other numerators the value of x/0 goes beyond not having a single defined result - there simply is no value 'y' such that y * 0 = x and there is no meaning whatsoever to be drawn.