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.
> From the paper, "Notably, for multiplying two 4 × 4 matrices, applying the algorithm of Strassen recursively results in an algorithm with 49 multiplications, which works over any field...AlphaEvolve is the first method to find an algorithm to multiply two 4 × 4 complex-valued matrices using 48 multiplications."
...but Waksman's algorithm from 1970 [1] multiplies two 4 x 4 complex-valued matrices using only 46 multiplications (indeed, it works in any ring admitting division by 2).
Sloppy by DeepMind and by Nature to publish such a claim - did they not ask someone knowledgeable about matrix multiplication to review the work?
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 looks quite similar like the "Lagrange models" defined by Joris van der Hoeven in https://hal.science/hal-01188378/document, a version of Taylor models where the constant error term is replaced by an interval multiple of x^n.
Representing functions locally is a very interesting problem: there are lots of possible approaches using intervals, Taylor series, Chebyshev series, etc. Big open design space if you ask me.
There is an algorithm by Richardson to prove equality of real and complex numbers composed from exponentials and logarithms. (It doesn't have a complete proof of correctness, but it never returns a wrong result: it will loop forever iff it encounters a counterexample to Schanuel's conjecture.)
It can also be extended to higher transcendental functions, but it gets harder to guarantee termination.
I have a library for exact reals/complexes with an incomplete implementation of Richardson's algorithm: https://fredrikj.net/calcium/
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).
My number one wish would be the ability to read definitions from .h files automatically. Other than that, I've had some issues with memory management with ctypes (objects being deallocated prematurely) that I never had with Cython, but that may just be my own fault. I agree about the lack of interop with Python ints.
I'd like to see optimizations targeting ctypes, or a successor to ctypes. I wish I could write elegant, performant C wrappers in pure Python. Right now the best choices are Cython, which is a hassle (separate, slow compilation, various warts), and ctypes, which is slow (and has some design problems of its own). Julia's ccall alone is a major selling point over Python right now.
This version of CM looks too thin. The version that comes with KaTeX (https://github.com/KaTeX/katex-fonts) looks great in the browser though. Would be nice if someone packaged that font in a more user-friendly way.