A 13-state Turing machine has been proven to halt in f_(ω+2)(f_ω(20)) steps on the fast-growing hierarchy, setting a new record for BB(13). Credit Jeff Ketchersid on Github.
165 points · 37 comments
after ~10 hours of work Astra simplified it to 252 states (proved in Lean)
github.com/VladimirReshetnikov/ProveIt/tree/d766f…
15 likes · 834 views
What the smallest one seems to be is here: github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m…
1 like
@JDHamkins github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m…
There is a proof in the Rocq theorem prover here.
PA was done in 238 states here:
github.com/jeff87654/busy-beaver/tree/main/PA/m238
I gave ChatGPT high-level suggestions for things to try or search for, and it did all the detailed work. Then someone else used Claude to formalize it.
I have the complete history, and I'm planning to write it up at some point. It changed the theory a couple times, but mostly worked by saving 1-4 states at a time from the current record in a loop.
I stopped optimizing only because I wanted a proof first, but now that I let it search again it already found a 253-state machine.
9 likes · 309 views
@_Mira___Mira_ an yup thank you, i found the github
github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m…
3 likes · 316 views
busy-beaver#18
One of my bots quickly finished up the PA proof after seeing this example.
So the 238th Busy Beaver cannot be proven in Peano Arithmetic.
The Metamath one I was working on had an extra step: Technically you need to embed the proof in a formal system to apply Godel's Incompleteness theorem, instead of just alluding to it conceptually.
But this approach is much easier.
2 likes · 1 repost · 245 views
github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m…
Someone else formalized my 254-state "halts iff ZFC is inconsistent" Turing Machine. Claude is really good for this, apparently.
So the 254th Busy Beaver cannot be proven in ZFC.
That leaves only the 238-state PA machine, which will probably come soon.
25 likes · 1 repost · 749 views
BB(10) > Graham's Number
BB(10) > Graham's Number (github.com)
Discussion | Main Link
BB(10) > Graham's Number
1 point · 1 comment
Mentions
A 13-state Turing machine has been proven to halt in f_(ω+2)(f_ω(20)) steps on the fast-growing hierarchy, setting a new record for BB(13). Credit Jeff Ketchersid on Github.
after ~10 hours of work Astra simplified it to 252 states (proved in Lean) github.com/VladimirReshetnikov/ProveIt/tree/d766f…
What the smallest one seems to be is here: github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m…
@JDHamkins github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m… There is a proof in the Rocq theorem prover here. PA was done in 238 states here: github.com/jeff87654/busy-beaver/tree/main/PA/m238 I gave ChatGPT high-level suggestions for things to try or search for, and it did all the detailed work. Then someone else used Claude to formalize it. I have the complete history, and I'm planning to write it up at some point. It changed the theory a couple times, but mostly worked by saving 1-4 states at a time from the current record in a loop. I stopped optimizing only because I wanted a proof first, but now that I let it search again it already found a 253-state machine.
@_Mira___Mira_ an yup thank you, i found the github github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m…
busy-beaver#18 One of my bots quickly finished up the PA proof after seeing this example. So the 238th Busy Beaver cannot be proven in Peano Arithmetic. The Metamath one I was working on had an extra step: Technically you need to embed the proof in a formal system to apply Godel's Incompleteness theorem, instead of just alluding to it conceptually. But this approach is much easier.
github.com/jeff87654/busy-beaver/tree/zf-254/ZF/m… Someone else formalized my 254-state "halts iff ZFC is inconsistent" Turing Machine. Claude is really good for this, apparently. So the 254th Busy Beaver cannot be proven in ZFC. That leaves only the 238-state PA machine, which will probably come soon.
BB(10) > Graham's Number
BB(10) > Graham's Number (github.com) Discussion | Main Link
BB(10) > Graham's Number