At high enough N, ZFC is independent of BB(N), and in fact any math axiom system has such an N.
The LLM itself is finite, the axioms it knows are fixed, there is an N where BB(N) is independent of those axioms, so the LLM cannot solve it.
2,485 karma · joined November 28, 2013
The LLM itself is finite, the axioms it knows are fixed, there is an N where BB(N) is independent of those axioms, so the LLM cannot solve it.
The proof verifier uses fixed math axioms. The busy beaver function at high enough N cannot be proven with those axioms.
LLMs are computer programs, so there are math problems which they cannot solve. AKA, ideas which are not possible for them to generate.
The argument for this is that Busy Beaver function is uncomputable. More specifically, some N-state Turing machine requires a proof that it doesn't halt. At some point N is too large and LLM being a computer program, it cannot generate the required proof.
See the Busy Beaver Frontier [1]
This is VERY DIFFERENT from the Halting Problem. In the Halting Problem, we see that no computer can decide whether an arbitrary given input program halts. With the argument above, for a fixed LLM, there is specific math problem which is beyond the capability of proof by the LLM (though other LLMs or humans could perhaps prove it).
Humans are not bound by the argument since we aren't finite computer programs (no proof for this anyways). LLMs which "evolve" over time with input from the natural world also aren't bound by this, since their code is effectively infinite. The argument only applies to a static program with fixed input, no dynamic information sources.
Some people believe in divine inspiration. Maybe you could believe that humans incorporate information from the natural world which LLMs don't have access to. Either of these beliefs would imply that humans have an edge.
The idea that when LLMs produce solutions, people won’t try to understand them and won’t learn from it, is obviously not true. Terry Tao himself spent time digesting and simplifying LLM proofs.
So again we’re left to speculate what the actual problem is.
Math understanding will increase with LLMs. Not just professional mathematicians but amateurs.
Most math textbooks have solutions in the back. That didn't wreck peoples ability to learn math, did it?
So we are left to speculate about why solutions in appendix are fine, but LLM solving open problems is not fine.
https://www.oca.org/saints/lives/2014/11/19/100292-saints-ba...
Most of the cost for agentic coding is input tokens, you pay for the whole context at each tool call or message. Output tokens is just a small rate
When I put Qwen3.8 27B xhigh towards adding scope proxying to the Guice library, it one shotted a great impl using 250k context before stopping.
Part of the greatness of the model is that it just keeps going until it gets a great result. 128k context is disappointing.
Memory-wise, the RTX PRO 6000 can barely hold two 1M context Qwen 3.8 27B models at 8 bit quantization at the same time. The 512GB M5 Ultra Mac Studio could hold around 14.
At such high concurrency, batch performance is usually limited more by memory bandwidth than compute. The RTX PRO 6000's memory bandwidth is just 50% faster than the M5 Ultra.
So yeah, I think if we are talking about many short context requests, sure. But if you are chewing through a backlog of coding tasks with Qwen overnight, they might actually be comparable.
Im sure in Nov when the M5 Ultra comes out we'll see a lot of interesting benchmarks.
Also, from what I can tell, MLX inference is not as well optimized as CUDA, and the M5 Ultra has additional kinds of AI compute which is unavailable on other M models. With the massive 1.2 TB/s 512GB Mac studios coming out, I think MLX will get a lot more attention.
In short: Todays models should run faster next year, and next year's models should also be more efficient.
Considering that I hit the 1M compaction multiple times per day with codex, it would definitely cost at least $5-8/day to use deepseek how I normally use codex.
Idk where you live, but where I am running the M5 Ultra Mac Studio at max rated power 24/7 for a month costs C$42.
The considerations against Apple hardware are 1) hardware advancements 2) early access to the best models. But it’s really not that clear.
(The other guy who thought hosted models on openrouter are cheap has spent $100k in 5 years.)
99% of the cost was in input tokens, I only used like 100k ish output tokens. It was a one shot task asking the agent to implement proxy injection to Guice. It did a pretty amazing job.
If you were to use hosted LLMs for a lot of agentic coding, a maxed out M5 Ultra Mac Studio would pay for itself in under a year.
That happened to me a few years ago. It was a very interesting experience.
It’s surefire subjective proof that aphantasia is real - the image I saw was so vivid and colorful, even animated. I can say for sure that I almost never have that experience.
At the same time, my one experience was surely in many ways much more limited than some others normal visual thoughts.
The mind is an interesting place.
GP isn’t suggesting that focused narrow model(s) will be more capable than large model, but that many small focused models can have sufficient capability while being more optimal.
Also, the bitter lesson is just wrong. The bitter lesson is about hand tuned AI vs computational general methods. However in truth today’s AI uses both. We have general compute heavy models which require narrow expert instructions (eg tools internet docs).
LLMs would not be as good without expertly written context, and expert context without LLMs aren’t as good either.
Honestly if you don't have working patches, it's really not owned.
I would love to get a better understanding of how to safely iteratively patch firmware. I bricked a router last week trying to add a TFTP boot path to the boot partition. It just sucks that it's so risky.
Relatedly, we also need good glitching tools, as some firmware even for cheap devices are not available unencrypted, and flash read is disabled...
We are NOT there yet but I hope we get there soon.
Their v15 release (apr 16) really enabled k8s native runners. They added an ephemeral runner API and a bunch of APIs to get jobs. That's what im using to do k8s autoscaling
It was a bit of a pain to configure firecracker with k3s.
It really can’t be understated how much easier hosting CI is with microvms as the security boundary.