Having worked with people doing bringup of specialized chips, I am awed at how the world has changed.
> When the first chips came back from the foundry in May, the team pointed its internal AI models at designing software to run benchmarks such as SemiAnalysis’s InferenceX. On DeepSeek’s multi-head latent attention kernel benchmark, performance climbed from 0.31 percent of the theoretical ceiling (set by the chip’s compute and memory bandwidth) to 88.94 percent in roughly 40 hours. Ho says this result is repeatable, so the time between when foundries deliver the first chips and when production ramps up can be reduced. “All our schedule assumptions are going to be based on the fact we have this capability now,” he says.
No, you forgot about the dependencies (others said it to be 700Mb). And 2,900 LOC is still way too much for handling a remote API call, especially in a high level language such as Python where the biggest part of the task is delegated to separate modules.
On the contrary, the readme for this project, `litelm`, is contrasting with the bloat project, `litellm`. This project subty deboats an L.
The bloat (or featuritis) project has the 700mb and 100k+ LOC, this de-bloat has 2k LOC and specifies its only two deps ones most people want as deps (although httpx should be swapped to its successor).
So this response is off base, the 700Mb isn't forgotten, it's been dropped.
Perhaps you did not understand the Fermat theorem proof announcement/repo or the link. The 13 million lines did not use any external, possibly not honest libraries, as the proof eventually only used the fundamental axioms. So for the Fermat theorem formalization, no open open questions remain.
The point is, they "proved" the Collatz conjecture. You would not know they exploited a bug unless you actually went and dug into their proof. Can we be so certain this has not happened within the millions of lines of Navier-Stokes? In an ideal world, our proof assistants would be more battle-hardened by now (recent exploits deny this), our AI better aligned (their tendency to cheat at tests denies this), or their handlers more responsible (the Hugging Face incident denies this), but the reality is more complicated.
At this point in time, we really can't be confident in accepting proof certificates without any human eyes on the script that generated it. I still have 95%+ confidence in this particular result being trustworthy, but a precedent of blind faith is guaranteed to end badly.
This person knew they did not prove the Collatz conjecture and others independently figured it out within hours. Not sure this is at all relevant, other than pointing out how trivial it is for the community to understand errors in lean4.
It was trivial because the Collatz proof script is literally 1000x smaller than the script for Navier-Stokes and involves no advanced math. And they found the bug by... manually inspecting the proof script. Maybe we should do the same for Navier-Stokes before declaring the matter settled?
Not only that, but there is a very fuzzable tell of something funny in the Collatz proof script (`CommandElabM`, i.e. metaprogramming). We may not at all be so lucky in other malicious scripts, especially if there are still kernel-level bugs in Lean.
I am not sure what you mean here. There exist plenty high-concern biological threats that dont need any AI help. Human oncovirus design is low on my concern list (immunity is diverse), and in any case it does not need AI—rather labspace. Disgruntled high schoolers or undergrad chemists can do way more damage from readily available materials without AI and without research delay. As can nature (or amateur biologists without AI) by mixing bats with their animal of choice and waiting a while. If/when any scary global events like covid happen again, I sure hope we have true superintelligence to help us navigate it quickly.
Other than the undeniable breakthrough in math, the important point is the ability to orchestrate 10k agents to productively work on a single problem, which creates options:
> OpenAI, meanwhile, says its experience with Navier-Stokes could open the door to solving puzzles with more practical relevance. “We are now able to spend millions of dollars on a problem that we really care about and that really matters: developing new materials, finding cures to diseases,” Bubeck said. “All of those things that we have been talking about for a long time—now they seem to be at our fingertips.”
With 10,000 agents and $20M of compute this is just brute force search.
It's a bit like telling 10,000 kids there's an easter egg hidden over there, pointing to one corner of your yard (or having "heard a rumor" it was hidden in that corner).
If you have $20M to spend on your problem, then yes, AI brute force search is an option, but unless you know a solution is possible (as OpenAI did here), you may still be wasting your money.
You jest and that is OK. Brute force search is not something you can do over math problems of that difficulty or anything with combinatorial complexity.
To me it feels closer to taking the top 10k human mathematicians on a large retreat for a year and having them self organize to collectively solve this problem—not kids and easter eggs.
I'm not joking. Compare to a super-human MCTS system like AlphaGo or Stockfish - once you condense the expertise of your top 10K world experts into a board evaluation or policy function, then the rest is brute force.
Whether this type of agentic swarm approach can be considered closer to MCTS (search), or closer to a less structured GOFAI blackboard type approach (perhaps more like your mathematician retreat) I'm not sure - I don't think they've released any details of the prompt(s) and how these agents were collaborating and building on each others work.
The other part of my easter egg analogy is the direction to "look over there", corresponding to OpenAI specifically asking their hoard of mathematicians to work on Navier-Stokes since they knew it was solvable/determinable, and they certainly had the public work that Buckmaster/Levant were building on as further direction, as well as perhaps their prompts. Unlike Buckmaster/Levant, this wasn't just a couple of humans with a university research grant budget, this was apparently a not-so-small team at OpenAI (says Buckmaster, per a group call he had with OpenAI), with an unlimited budget, so it's hardly surprising (or in the least bit impressive) that they were able to duplicate and surpass their work.
I agree with search, which is what mathematicians also use over longer periods of time. But it is not brute force search (and neither is alphago’s search or modern stockfish, though both still search at depth and speed higher than typical human).
If you can create a graph of independent work, which you can with many such problems, agents can work together nicely. Again, thank Lean and the tooling around it.
That was the net effect (assuming what they solved was the actual problem and not a loophole in the problem statement or a lean bug). My point is they need not all work coherently to do that -- for example, for all we know 3/4 of them went off the rails, their results were pruned, and the relevant results came from a random subset that happened to produce something useful.
If you work with distributed systems, you still call that scenario a success. On the other hand, if the 3/4 of agents going off the rails bring down the whole mission, that is a failure. The latter would have been my guess with current models scaling to 10k agents.
I am not an expert in lean4, but I could follow parts of the high level lean definitions of the problem statement in the repo. A lean bug would be a fun scenario; I am certain this proof will receive the deserved scrutiny, and if it uncovers a bug, it will make the story even more exciting. It is extremely unlikely to be the case, however, because the 10k agents working on the proof didnt use lean, so it would have to be a math logic error that translates to a lean bug—perhaps something the agents picked up during training?
> When the first chips came back from the foundry in May, the team pointed its internal AI models at designing software to run benchmarks such as SemiAnalysis’s InferenceX. On DeepSeek’s multi-head latent attention kernel benchmark, performance climbed from 0.31 percent of the theoretical ceiling (set by the chip’s compute and memory bandwidth) to 88.94 percent in roughly 40 hours. Ho says this result is repeatable, so the time between when foundries deliver the first chips and when production ramps up can be reduced. “All our schedule assumptions are going to be based on the fact we have this capability now,” he says.
reply