fdej

If you don't want to allow division by 2 then there is Winograd's algorithm from 1967 which works over any commutative ring and uses 48 multiplications for 4 x 4.

There's no a priori reason why the expected success rate of research projects should be 50% and not, say, 1% or 99%.

That is the way the FLINT fmpz type does it. The benefit is that you can check for pointers once and then use the operands like ordinary ints without the +1/-1 adjustments. For example, to multiply two integer matrices, you can do O(n^2) pointer checks and then do O(n^3) arithmetic operations without overhead. But if the pointer check is done each operation then the representation doesn't make much difference; whether you use the LSB or MSB as a tag, what kills performance is checking and branching based on a tag bit in the first place. What you'd want is a sufficiently smart compiler (TM) that can eliminate as many such checks as possible.

This is indeed the issue. Using provable bounds loses too many bits for complex FFTs to make sense for long multiplies.

No, this is wrong. Richardson's theorem is about functions, not constants. Equality of constants constructed from exponentials and logarithms is decidable (assuming Schanuel's conjecture) by another theorem (and algorithm!) of Richardson.

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.

Correcting myself, the bound is worse than exponential (so read "at least exponential in N"), but the point I wanted to make is that it is explicit.

Again, this follows from the general theory of algebraic numbers: the degree and height of a sum, product or root of algebraic numbers can be bounded explicitly (resultants + Mignotte bound for factors), and finally root separation bounds can be applied to the resulting polynomial.

Yes, the worst-case complexity is exponential in N, but the wording in the article could lead you to believe that no explicit exponential bound is known, which is false.

> But how long will we need to look through these sequences of digits before we find the disagreeing digit? It feels intuitively like we should be able to establish some kind of bound on this. Like, maybe we should be able to say “if you add two lists of n numbers, each of which has d digits, then they can’t disagree for more than k * n * d digits” for some k. But no-one’s been able to prove anything like this.

You can write down a completely explicit bound here using the Mahler-Mignotte root separation bound. More generally, for any algebraic expression involving algebraic numbers, you can bound a priori the number of digits you need to check to determine its sign.

When you involve transcendental numbers, things do get much harder though.

Yes, indeed, and Strassen is a bad default algorithm because of this. There are specialized situations where the numerical stability isn't an issue though.

What makes you say that? I've had good speedups with Strassen multiplication in variable precision (or with floating-point, in case you meant fixed-point arithmetic).