srcreigh

I think there's a really important sense in which Godel's argument is not the full story.

IIUC, Godel's incompleteness is less about theorems and more about axiomatic systems. Given an axiomatic system, there are statements within it which cannot be proven or disproven. It's relatively unrelated to the platonic ideal of the theorem itself. The statements it considers are axiomatic-system-specific.

Another way to view it is, who cares if we can't prove or disprove "This statement is false". Ok, the axiomatic system is incomplete; fine. What's important is can the system prove a real theorem that I care about.

The busy beaver computability argument addresses these issues. The problem format is always "For Turing machine T with no input, does T halt?". This format can encode many math problems. And we know already that BB(432) is independent of ZF, aka, there is a 432-state TMs which ZF can't prove or disprove the halting behaviour of.

So BB looks at real theorems, ranks them, and we can ask what axiomatic systems can solve them or not. Godel looks at 1 axiomatic system and produces a toy theorem which the system can't solve. That's an extremely important difference!

The core issue is that any fixed LLM can only encode so many axiomatic systems in its states, and the fixed systems implies an upper bound in terms of the BB number which it can solve. Godel is only looking at one system at a time, while BB is a way to use a common problem format to rank every axiomatic system on an infinite number line.

It's impossible for finite number of LLMs to solve all theorems. This would imply that the busy beaver sequence is computable which implies the halting problem is decidable.

For any finite program (eg some LLMs), there is a true math theorem which they cannot prove or disprove (given fixed input of the statement with no other information sources). If that weren’t true, BB would be computable.

Math is beyond computation. Since AI is just bits in bits out, it has this fundamental limitation.

Any magic of AI systems comes from the transformed meaning of its input data. With fixed weights any LLM is just an artifact. For example a human prompting an LLM constitutes an extra information source, which removes the above limitations. In theory any input from the natural world would remove the limitations too. The natural world is a black box and we don't know what kind of meaning or intelligence could underly it.

Not firecracker

Nope, there is no such universal logic. Godel helped show the opposite actually (incompleteness). I think Scott Aaronson's post is very fascinating explanation of this stuff. https://www.scottaaronson.com/papers/bb.pdf

The point is that some statements could be provable, but not with today's proof verifier.

"Everything that can be proven" is relative. PA can prove some things, ZF more things. In 200 years we could develop more powerful math foundations which can prove more things. Today's proof verifiers could never prove them, but tomorrow's proof verifiers could. And the cycle repeats.

The point is that it has limits in what tools it can use by virtue of being a finite program. Those limits imply that there are some math problems that it cannot solve. The LLM can know about this (and frontier LLMs likely do), but that doesn't mean it will be able to solve the math problems.

To put another way, if it were true that some fixed LLM could solve every math problem, it would implement Halt, which is impossible.

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.

No, but you hit the nail on the head, that’s the most interesting part.

The proof verifier uses fixed math axioms. The busy beaver function at high enough N cannot be proven with those axioms.

> I think it’s broadly unclear whether (3) is true: i.e. whether frontier AI models aren’t generating or can’t generate new mathematical ideas. ... I give basically zero credence to the idea that AIs are incapable of this because of some intrinsic feature of how LLMs work.

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.

[1]: https://www.scottaaronson.com/papers/bb.pdf

What do you think the concrete problem is?

LLMs can help people understand mathematical principles too.

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.

Yeah. This makes sense. Someone who can dedicate a lot of time to scaling a SaaS serving many customers are helped a lot by AI. I believe busy professionals who already have successful businesses won't have the focus to build a one-off solution for their own needs a lot of the time.

No, this cannot be the actual issue.

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.

At least for now, not everybody can make a private SaaS. Doing that requires skills and focus. Even with SOTA models, as of ~today, there are inflection points where the AI would not be able to make the right choice without a knowledgable human, or would cycle and waste time with things that don't matter, etc.

Without pinning providers, you pay let’s say 2x more for agentic coding, since that many input tokens aren’t cached as you bounce between providers.

Math can never be fully solved by a computer, if only for lack of computational resources.

The OCA (Orthodox Church of America) has a hagiography page regarding them.

https://www.oca.org/saints/lives/2014/11/19/100292-saints-ba...

How many years until chips like this are available to consumers?

It is 15x more expensive. Openrouter usually charges like 1/4 for cached input.

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

Great observation. That’s not enough context even for some one shot xhigh requests.

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.

No, I don't own any of this hardware, im just summarizing what I could find by reading others posted benchmarks

There is comparison actually. I spent all day researching this a few days ago.

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.

Makes you realize how insane the M5 Ultra Mac Studio is. 1.2TB/s bandwidth 512GB memory. Its rated max power draw is just 480W. And it also has amazing M-series CPUs. It costs less than just one of these GPUs which each take 700W to run.

The adults brainwashed us

https://www.ikea.com/ca/en/p/barndroem-box-beige-70560615/

https://www.ikea.com/ca/en/p/vallaby-rug-green-10548216/

Open weight models have been getting better/smaller every year.

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.

So I ran the math, assuming the agent takes 75 turns per 200k context, with deepseek v4 flash it costs around $2.57 to reach 1M context in 375 turns. Cached input costs scale quadratically with # of agent turns.

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.

It’s not so clear after 5 years that you’ll come out ahead. You’ll have spent $20k. The apple computer owner will probably be running local models that are better than today’s frontier on the same hardware.

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.)

They're not cheap at all. I did one xhigh Qwen 3.8 27B agentic coding task last week via OpenRouter and it cost me like $10.

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.

Well, yes, but if k is for example Ω(n) then O(n-k) is also O(1).

Do any other aphantasia folks have the experience of like, that one time they saw a very vivid image, but it only ever happened once for a short time?

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.