At the time that the Millenium Prize problems were formulated, the force term was understood to make the problem more realistic, since real fluids are always going to have external forces applied to them. A blowup that happens under constant gravity, for example, would probably be no less interesting than an entirely unforced blowup. The strategy of constructing impossibly complex external forces to induce a blowup was pioneered by Córdoba and Martínez-Zoroa only over the past few years.
Today that point is moot because.. including this one, the Mill problems that are most likely to have been solved are least likely to have real world impact..
Extrapolating on that, I'll take on the biased hope that almost none of the 100 solutions to be released will have any applications for at least 30 years.. (besides PR wins for AI companies)
In order to counter the fear (my own lonely one) that the 9 big names will not be able to hold the execs to account or get openAI to act "more responsibly" (whatever that means).. in the form of direct hits to new subs or partnerships or funding
I plead guilty to any accusations of (vicarious) sour grapes or sympathy for the weak
Point to you, because.. the committee would make more sense if they also bring Ant to the table.. unfortunately nerds will be nerds, so perhaps, to you, and I'll reluctantly concede, mathematicians deserve to be serfs
Exactly! One effect of the committee might be to benefit Ant by its presence alone.. if only by striking fear in OpenAI.. Ant don't even need to thank them at once
Let's say they do not much on Ant's findings but edge on the NDA with OpenAI. That might even be PR victory for mathematicians
>Are there any notable classes of programs/problems where you'd do an LU decomposition of this specific matrix?
It doesn't have to be this specific matrix. If it's some service exposed to the internet, it can be user supplied, in which case it turns into a backdoor.
You could combine it with existing products like DevonThink that are meant for researchers organizing documents and provide tagging, semantic search, similarity graphs, and so on.
So an encoder-only model with a classifier trained on the heads or something? DeepSeek recently switched to an encoder-decoder architecture in an attempt to get the best of both worlds (fast prefill while preserving generation capability), I wonder if that might be the future?
>This spills over into other processes wanting to use the GPU, namely the WindowServer.
Why does this spill over? Unlike CPU which is multiplexed by the kernel's scheduler (so infinite loops can't lock out other programs), is the GPU not multiplexed in the same fashion?
Often not in the same way - even if there are multiple queues (that can be given a priority), they're often limited in what they can schedule between.
Often there's shared resources that are statically allocated to shaders (register space, local memory etc.) that means you often can't "just" add a new task if those shared resources are already in use. But not using those resources to their full would cause performance issues.
And the internal state of a GPU is often very large, much larger than a CPU, so suspending the current tasks, saving out their state and replace it with a "higher priotity" one can be very expensive - so often an afterthought of support at best.
Otherwise GPUs typically do context "pre-emption" by basically being cooperative and just injecting yield statements in the command queue or on things like tile boundaries for tile based renderers. So the smallest chunk of work they can yield between ends up actually being quite large, and with a full user-supplied program in the middle
you can get another LLM to verify / if the lean doesn't have `sorry` used to skip certain parts of the proof etc. It's much easier once it's in lean4 because checks like that can be done computationally.
Then why was it allowed as an option in the millennium prize statement?
reply