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?
1. Waksman's algorithm works in any commutative ring admitting division by 2.
2. In particular, it won't work when the matrix entries are themselves matrices, which means you can't use it recursively to get an algorithm for n-by-n matrices with large n with a better exponent than you get from Strassen's algorithm.
3. The Deep Mind paper is annoyingly unexplicit about whether the algorithm it reports has that property or not.
4. What they say about tensors suggests that their algorithm can be used recursively to do better than Strassen (but, note, there are other algorithms that are substantially better for very large n which using their algorithm recursively would very much not outperform) but it's possible I've misunderstood.
5. They explicitly talk about complex-valued matrices, but I think they don't mean "complex numbers as opposed to matrices, so you can't do this recursively" but "complex numbers as opposed to real numbers, so our algorithm doesn't get you a 4x4 matmul using 48 real multiplications".
I am not certain about points 4 and 5. The language in the paper is a bit vague. There may be supporting material with more details but I haven't looked.
2. Correct, however you can use Waksman as a basecase and always beat Strassen (though it is not asymptotically better of course).
5. Possible, but even so, there is already an algorithm that will work with 46 real multiplications (and some divisions by 2). The real numbers are commutative and admit division by 2.
My point about #5 was just that their emphasis on "complex numbers" isn't necessarily (and I think probably isn't) an admission that their algorithm can't be applied recursively.
If it can be, then it is a genuine advance in the sense that it yields faster large-n matmuls than were previously available just by recursive application of a 4x4 matmul algorithm.
None of which, to be clear, makes it OK that they don't make any mention of earlier work that does 4x4 matmuls over commutative rings faster than their algorithm does. I suspect they didn't check the literature carefully enough before publication. In any case, good scholarship means being clear about what in your work is a genuine advance on what's already known and what isn't, and they failed to do that here.
> There's no a priori reason why the expected success rate of research projects should be 50% and not, say, 1% or 99%.
Humans are really bad at predicting the future, so I'd argue that the large majority should be between 49% and 51%. A 99% success rate would imply that humans can predict the future, which I think is pretty much the opposite of how science should work.
I would actually put it 60-80%. As there is plenty enough of ideas that should work. It is not really random search, but applying existing knowledge or expectation to some different area. If doing one thing with one thing works, I would fully expect in many cases that doing same thing with this other thing relatively closely related to also work.
Lot of research is iterative process and there you can do iterations that you know could work and already ignore things that certainly won't.
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.
