Would rewriting Linux to seL4 standards cost $16B in the world before or after frontier models are solving Erdos problems?
After. (EDIT: For the incredibly basic reason frontier models are already solving Erdos problems, but the largest LLM-based piece of system software is only borderline functional dumpster fire of a C compiler, but keep reading.)
It’s fantastically impressive that LLMs can solve Erdos problems! But:
Erdos problems are much smaller than the Linux kernel, and much easier to verify. Both these factors play to LLM strengths.
Not all Erdos problems are equally difficult. Some seem to be just difficult enough that a human would need to seriously dig in and grind it out, or bring a nice insight from a distant corner of math. Others are likely more difficult. I believe about 551/1217 are currently solved.
Reimplementing a highly-secure kernel that could replace Linux for most uses cases is an enormous project with many poorly defined subtasks, which is basically hell for LLMs. The biggest LLM project I’m aware of is a C compiler. Which basically works, but which is apparently a remarkably terrible C compiler. And C is far, far better specified than the internal guts of Linux and all the ghastly hardware that Linux supports.
Also, please keep in mind that I’m willing to handwave a couple of zeros either way on the larger estimates.
I expect overall security of newly written code to get clearly worse on average (thanks to the deprofessionalization of software development and companies pushing vibeslop to production) right up until offensive Mythos-class abilities become widespread. Then I expect things to get unpleasantly exciting.
Ah, yes. That Hideous Strength. A strange novel, certainly.
I’ve long felt that it was about the Singularity, as seen from a primarily biological perspective. You see the dreams of power and transcendence, the early partial successes, and the inevitable corruption of nearly all the people involved. There’s even a discussion of s-risks. The ending is positive because C.S. Lewis wanted to tell an entertaining story, and because his religion encouraged him to believe in impossible last-minute grace.
I may have referred to various AI labs as “the National Institute for Coordinated Experiments” in the group chat. I suspect that they employ more than one Filostrato, Wither or Frost.
Google once prided itself on “Don’t be Evil,” and they even sometimes lived up to it, to some degree. But money and power have corrupted them pretty thoughly, over stakes no higher than some ad revenue. And one of the arguments of That Hideous Strength is that people who push for a Singularity are unusually corruptible, because the temptations are so great. And, frankly, because they would need to be unspeakably arrogant and reckless to try.