lg5689

Are you thinking of the int multiplication result instead? The DFT result uses a computation model with unlimited precision reals.

Quant finance is very different from math research; quant is much more applied math and programming, and the tasks are typically smaller than math research questions. Although it's true there's a huge overlap in the people good at both, there is massive re-training needed if you want to turn non-math-phd quants into research mathematicians.

As I argued in another comment here, I think even with unlimited budget, humans wouldn't be able to reproduce these results within a few years. I think AI has crossed a superhuman theshhold in math problem solving skills.

As for #2, personally I feel like OpenAI's results are superhuman at this point. I don't think there's enough human talent alive right now to produce these sorts of results within a few years, no matter the budget.

There are lots of reasons I believe this. One is that frontier AIs are very clearly superhuman on shorter problems (as can be seen on benchmarks like FrontierMath, or just by playing with them yourself if you have a source for difficult problems)--so these achievements are "just" scaling that advantage to research-sized problems. Second, AI is also clearly superhuman in its knowledge across fields, so it can make connections and combine techniques that humans won't be able to access. Third, these problems are famous and have withstood efforts of many of the best humans, in many cases being considered unapproachable.

Altogether it seems like AI is not only smarter but also more cost efficient that humans for math-adjacemt problem solving. I'm not saying that AI is superior at everything in math, eg theory building, but I think it's really unlikely you could get any group of humans that could compete with OpenAI's latest results.

This is integer multiplication, not matrix multiplication. The OpenAI dump also has a matrix multiplication improvement though.

In either case, no practical algorithm is expected to come from it, because the asymptotic gain isn't realized for practical input sizes--sometimes called a "galactic algorithm". But it's theoretically very interesting for breaking through a conjectured barrier.

I think it makes sense to feel sympthy towards people facing disruption in their plans, even if you believe society is better off overall.

It's like getting scooped. If you just founded a startup based on tech XYZ, should you be happy when someone releases an open source XYZ? Should a news reporter be happy when another network breaks the story they were working on? On the one hand, society got the value of the thing you wanted to do. On the other hand, now you need to find something else to do, which might be really annoying.

This is a legitimate question, and it'll be interesting to see how these constants evolve in the future. In some cases, maybe it's true the AI did the minimum to break the barrier, and the best constants are much lower. It's still a notable result that the barrier was broken. But it's quite possible that there's not actually much more to improve.

Many of these latest results are very important to theoretical math. Some are also theoretical physics and CS.

Real-world applications are far off, but developing mathematical understanding does tend to leak over into applied physics and CS.

A cynic might say this is all just intellectual games, and though there's a grain of truth, it's too cynical imho. This isn't like 8 queens where there's no hope for applications or generalizations. A lot of this stuff fundamentally affects our understanding of how numbers and systems behave, what are the limits of computation, etc.

Even if someone doesn't care about theoretical results, it's still exciting that AI has become superhuman in a domain as broad as math. That shows there's potential to be superhuman in other domains as well.

It doesn't have to want to kill humans; indifference is sufficient. There's an exact analogy with humans: we have caused extinction and endangerment for many species, not out of malice, but indifference.

There are also many plausible arguments why our ability to train them to be helpful/trusting/aligned can fail. The smarter AIs get, the harder it is to be sure they're trained correctly. There are already reports that AIs are able to detect whether they're in a training environment and change their behavior accordingly.

Even if these are low probability scenarios, the risk-reward is terrible, so I think it's rational to be extremely cautious about AI risk.

AI vs AI chess, played from the standard opening position, is pointless--it's always a draw. Human vs human chess is doing well but AI is banned from it.

The chess-math analogy would imply AI could bring us into a golden era of math competitions for humans. But I don't think it says anything good about prospects for humans in research math.

Tbh this sounds perfectly normal to me. Companies often don't think it's worth defending themselves if theres no actual financial damage, and certainly don't want random employees to be doing it. It can be very frustrating, both for employees who want to defend their reputation and for the public who want the truth, but companies can be extremely conservative about chosing their public relations battles.

IANAL, but yes, I'd assume the license is unenforceable on the AI content.

No, an AI's output can still violate copyright.

LLMs are indeed very special compared to past efforts at automated theorem proving. The search tree for proofs is enormous, even short textbook exercises (i.e. a few dozen lines of Lean) were difficult with GOFAI techniques. Adding a few orders of magnitude to your compute budget barely moves the needle, since the search space increases exponentially for every line of the proof.

Now LLMs have produced multi-thousand line Lean proofs. This is impossible by simply "try everything and see what sticks". LLMs are able to target their efforts to only promising proof strategies. Yes it helps that they work at superhuman speed, so they can try thousands of strategies where a human might try a dozen. But their results cannot be explained only by compute increases; they need genuine mathematical insight.

There was recently an announcement that a group trying to formalize it found a gap exactly where other mathematicians were pointing. So to the extent there was any doubt, it should be gone now--the proof was incorrect.

But I agree LLMs have a lot of potential for checking proofs--both informally (they can read quickly and find gaps) and formally (by attempting to formalize).

I believe that "single source of truth" is a principle that should always be followed. If there's duplicated code where it'd be a bug if they diverge, then you should refactor. It creates a long-distance coupling in your code that may be invisible to future developers until a bug emerges.

But with that in mind, I mostly agree with the article: if it's not a violation of "single source of truth", then abstractions are just a convenience. If it starts being inconvenient, then it's not doing its job and there's no reason to use it. It's a serious code smell if a function needs several flags for custom behavior; that means it's probably the wrong abstraction or violating the single responsibility principle. If there is a legit need for lots of customization, an often-good way to handle is to take a function/functor as an argument for the customization. E.g., rather than `solve(f:double -> double, max_iters = 99, x_abs_tol = 1e-15, x_rel_tol = 1e-15, ...)` you can do `solve(f:double -> double, stopping_criteria: StoppingCriteriaClass)`