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.

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] https://doi.org/10.1109/T-C.1970.222926

Just check for the existence of at least one odd digit mod 10^B for some well chosen B.

Here is a C program that does the verification up to 2^(10^10) in 30 seconds: https://gist.github.com/fredrik-johansson/8924e10e5d74e39109...

Edit: made it multithreaded, goes up to 2^(10^12) in nine minutes on 8 cores.

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.

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).

I'm the poster. I think you misunderstood the followup post -- the same library is definitely used in the Cloud (same as the standalone Mathematica).

Indeed. There's no way for users of Wolfram Cloud, for example, to see that information though.

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.

I don't know why people complain about the new design. It has been a very effective cure for my reddit addiction.

Chick Corea was my gateway drug to jazz as a teenager, after my guitar teacher gave me Spain to practice.

A lot of musicians have the playing chops but few do truly interesting and original work as composers. Chick Corea was one of those.

Some of my favorite tracks, off the top of my head: Spain, Captain Marvel, Armando's Rumba, Sicily, Samba L.A., The Slide, Leprechaun's Dream, North Africa, Eternal Child, Tumba Island, Got A Match, Charged Particles.

The last track has some special significance to me since I listened to it repeatedly to pump myself up for a big life decision.

Plus, I have fond memories driving my parents crazy on roadtrips by playing "that crazy music" (= either Chick Corea or video game soundtracks) in the car.

That's a great question. Of course, you can express the computation as a function or a symbolic expression and evaluate it using a function that recomputes with greater precision automatically (or automatically compiles efficient code with bounds). Integrating this kind of functionality into the core semantics of a programming language is a very interesting problem.

Should be fixed now. Thanks!

The library doesn't support this directly. What you can do for normed vector spaces over R (or C) is to use the number types of Arb for the coordinate vectors, implementing your own norm and metric functions for the vector space on top of this. It's fairly easy to do since Arb handles all rounding errors in the underlying real arithmetic.

I think the name "ball arithmetic" is Joris's idea. I don't have a good reference at hand, but I believe the idea of using a centered form of intervals is as old as interval arithmetic itself. Ball arithmetic has been used quite a bit for complex interval arithmetic, where it sometimes offer better enclosures than rectangular intervals, and another nice point of ball arithmetic is that it generalizes to more general normed spaces. However, before Joris's and my own work, I think very few people realized how useful ball arithmetic is specifically for arbitrary-precision arithmetic.

Good point. I added an RSS feed link to https://fredrikj.net/blog/. I just hacked together some quick code to generate it, so let me know if it doesn't work.

This has various names: double-double, quad-double (etc.) arithmetic; floating-point expansions. It's definitely the best way to do arithmetic at precision up to a couple of hundred digits on modern hardware, though traditional arbitrary-precision arithmetic wins at higher precision (and in any case becomes necessary, due to the exponent range).

It's unfortunate that this isn't something that was standardized and more widely available a long time ago. By contrast, IEEE binary128 and binary256 are practically useless due to lack of hardware support.

For anyone wondering about the difference between endpoint-based interval arithmetic ([a,b]) and midpoint-radius ([m +/- r]) arithmetic (ball arithmetic): they are often interchangeable, but they have different tradeoffs. Roughly speaking, standard interval arithmetic is better for subdivision of space, while ball arithmetic is better for representing individual numbers.

A good technical introduction to ball arithmetic is this paper by Joris van der Hoeven: https://www.texmacs.org/joris/ball/ball.html

Author here. I will take the opportunity to advertise my blog at https://fredrikj.net/blog/ where I post occasional development updates about Arb and other projects.

Some improvements not covered in the 2016 preprint include much faster code for arithmetic and matrix multiplication (https://arxiv.org/abs/1901.04289, https://fredrikj.net/blog/2018/07/high-precision-linear-alge...), and code for rigorous arbitrary-precision numerical integration (https://arxiv.org/abs/1802.07942, http://fredrikj.net/blog/2017/11/new-rigorous-numerical-inte...).