12 Comments
User's avatar
lcamtuf's avatar

Note that most of the proofs cited in this article have something in common. They don't actually show the thing they claim to prove: they posit that there are only two choices and then rule out the other option.

This can be tricky; it leans on the principle of the excluded middle (PEM): "it's either x or not x". But can it be neither? Can it be something else? Maybe there's some third category between "stops in finite time" and "continues forever", and we just need a theory of that?

Although most mathematicians play fast and loose with PEM, there's a niche school of constructivist mathematics that treats many such proofs as unsound, or at least highly suspect.

Expand full comment
Cameron Mitchner's avatar

Great article. But are you calling this a toy?

https://en.wikipedia.org/wiki/ZX81

Expand full comment
lcamtuf's avatar

I grew up with ZX Spectrum 48, so of course we considered ZX 81 to be a joke.

Expand full comment
Cameron Mitchner's avatar

But then the Spectrum was the one with a fancy rainbow on the keyboard, so...

LOL - I coughed up good money for my 16K RAM expansion kit!

Expand full comment
Wyrd Smythe's avatar

This was an excellent and clear overview. Worth reading and then coming back to read again.

Expand full comment
Iustin Pop's avatar

me → this article → (woosh). Or at least after the "A constrained-instruction computer" part.

Expand full comment
lcamtuf's avatar

I revamped that section and the following one a bit, so it might be worth another shot!

Expand full comment
Iustin Pop's avatar

Ah, thanks, appreciated, but I think it's more on me than on you - I haven't done theoretical math or CS in decades.

The rewritten version is indeed more readable, but not really grokable. I see what you're saying, but I'm not able to follow well - I'm not sure for example, whether the BB(25) for Goldbach's theorem was an example or the actual number.

However, even from afar, your equivalence of the know-ability of BB(x) with Gödel's theorem is very interesting, even as a theoretical concept. Thanks!

Expand full comment
lcamtuf's avatar

Ah yeah, that "for example" should have been "in particular" =) Anyway, thanks for the feedback - I do try to write for myself from before I learned about a particular concept, but it's hard to nail it.

Expand full comment
Ruqya Chronicles's avatar

LLMs can do a nice job spewing proofs and symbolic notation but what good are thinking machines when we can’t define our problems in ways they can reason about?

Try using the Turing machine to calculate the equivalent of a sine (over a finite field - no unit circle) in Norman Wildberger’s rational trigonometry.

Computability and number theory is an increasingly important topic it seems.

Expand full comment
mids's avatar

I think it's interesting that in your constrained-memory brute force solution you didn't consider a computer that can observe (and influence) the state of another, but not the other way around. This exists in the real world, but can also be thought of as an emulator or debugger.

I digress, though, as it's not what you're going for in the article :)

Expand full comment
lcamtuf's avatar

It does, but it requires enough resources to represent the state of that emulated machine *and then some*. Note that I'm using "state" here in a sense broader than the state register of the Turing machine: it's the totality of the mutable universe of the computer.

If you use a computer to emulate itself recursively, you don't run out of "compute", but you run out of RAM.

Expand full comment