PS. I can have this view while simultaneously thinking that Ben is a badass.
To put it another way, the constants inside a big-O are not really constant: they depend on what you assume is a constant-time operation.
It seems like rather than coming up with more "galactic" algorithms, a more useful thing to do might be to come up with a replacement for big-O that's not so exploitable, and to convince theoreticians to play that game instead.
Doing theory is what gives you a chance to push the envelope to places you can’t even imagine when you’re knee deep in real world problems. And proving something is possible (if impractical) gives an incentive to find a better algorithm and may attract others.
For example see the first graph here: http://klotza.blogspot.com/2016/06/the-fall-of-twin-prime-ga...
Much of our 'practical' understanding of algorithms also in part came from theoretical advances.
You don't need to care. But every so often breakthroughs in theory can be turned into breakthroughs in practice.
> It seems like rather than coming up with more "galactic" algorithms, a more useful thing to do might be to come up with a replacement for big-O that's not so exploitable, and to convince theoreticians to play that game instead.
There's plenty of replacements.
Btw, we already have the optimal (in big-O terms) algorithm for every NP hard problem. We just don't know whether it runs in polynomial time or takes longer. And, yes, that algorithm called Levin's Universal Search is a galactic algorithm. Simplifying a lot, Levin's Universal Search does some clever interleaving to essentially try all possible algorithms in sort-of parallel.
Lo and behold, even the theorists you complain about don't see that 'loophole' as a solution, declare victory and go home. They still keep researching.
The problem is that proving an algorithm is necessarily galactic is incredibly hard. If you knew how to do this, you would become one of the most celebrated complexity theorists of the age. Stanford would be calling.
It's extremely hard to know what mathematics may be useful in the future or not.
That unintentional mockery of a repo is 262million lines of such moves and growing. I don’t think for a second anyone involved has a clue about complexity theory though or they’d just jump to the obvious “O(1) time complexity using an O(2^n) lookup table to cover all possible n bits of input” which is the final end state of Blums speedup theorem.
edit: by "things equivalent to" I really mean universal register machines, something that operates on integers and not directly on real numbers.
At most you use them for stuff like P vs NP, because Turing machines are 'only' polynomially slower than register machines, so it doesn't matter.
But when you are talking about linear vs quadratic on something resembling real computers, Turing machines are the wrong model.
There is, of course, the very rich field of Numerical Analysis which deals with how we actually represent these things in real life, but for a starting point assuming this sort of thing is par for the course.
Related, another article about proofs that may depend on bad formalizations:
https://news.ycombinator.com/item?id=49994145 - Navier-Stokes Lost in Translation (5 days ago, 237 comments)
AI seems to be very good at getting answers, but not always answers to the correct questions. These remind me of Deep Thought from The Hitchhiker's Guide to the Galaxy, where they got an answer to the ultimate question before actually knowing what the ultimate question is.
I don't think that's an accurate summary of the article you linked. The Lean proof solved the exact problem it was supposed to, it just had minor discrepancies from the writeup of the proof (on the level of saying a theorem requires m+4 derivatives when it actually requires m+5 derivatives). Obviously a problem but not really a bombshell.
As the argmin suggests Writing computational complexity in Big O isn't great here.
since we generally see the interms of no.of complex additions and no.of Multiplications in the FFT algorithm.
Err... doesn't that completely invalidate the big-O analysis!?
I suspected that these Open AI "proofs" of sub-nlogn times were cheating somehow, by sweeping something under a rug. This seems to be it!
This is a common thing in complexity, and I think even the abstract says it is talking about “length n” and not “magnitude n”
" In 1973, Jacques Morgenstern proved that you couldn’t get a Fourier transform faster than ½ n log n if you required that complex coefficients used in the computation had bounded magnitude"
I highly doubt this is going to somehow inspire people to make faster algorithms than the mathematical bound...
I have no problem with pure mathematics, my training was in it; but it seems very possible to me that most people funding theoretical computer science (as opposed to pure maths) probably assume the work has a more realistic computational model backing it up.