2024 claim of BB(5) (Was: FYI: The Busy Beaver Frontier / Scott Aaronson )

From	Mild Shock <janburse@fastmail.fm>
Newsgroups	comp.lang.prolog, sci.logic, sci.math
Subject	2024 claim of BB(5) (Was: FYI: The Busy Beaver Frontier / Scott Aaronson )
Date	2025-12-02 00:22 +0100
Message-ID	<10gl7vh$u4i2$1@solani.org> (permalink)
References	<10ghdp5$tg19$1@solani.org> <10gl1cc$1nhqt$1@dont-email.me> <10gl7ga$u4cc$1@solani.org> <10gl7n7$u4e9$1@solani.org>

Cross-posted to 3 groups.

Show all headers | View raw

Hi,

Here is a 2024 claim of BB(5)

Skelet #17 and the fifth Busy Beaver number
Chris Xu
We prove nonhalting of the Turing machine dubbed "Skelet #17", known to 
be one of the toughest 5-state, 2-symbol Turing machines to analyze. 
Combined with the efforts of The Busy Beaver Challenge, we are therefore 
able to show that BB(5), the fifth Busy Beaver number, equals 47,176,870.
https://arxiv.org/abs/2407.02426

Thats before 2025. But dunno whether its flawed.
Maybe the 2025 paper has has the meric that some proof
was computerized. While the above paper carries

proofs more informally. Maybe feed it into an AI
and you get formal proofs, dunno. Maybe?

Bye

Mild Shock schrieb:
> Hi,
> 
> I suspect to make a serious Coq endeavour,
> I would still study first:
> 
> The Busy Beaver Frontier / Scott Aaronson - 2022
> https://www.scottaaronson.com/papers/bb.pdf
> 
> But the above paper is also 22 pages. So
> not a 5 minute read,
> 
> Bye
> 
> Mild Shock schrieb:
>> Hi,
>>
>> Meanwhile I have found some papers where some
>> earlier lemmas are proved, that didn't make it
>> into the Coq proof. So I am not sure
>>
>> whether Coq is the first. Seems there are
>> different proofs possible. But I didn't spend
>> enough time on the matter, to explain
>>
>> details. Still in the collection phase.
>>
>> Sorry that I am not an excellent help here.
>>
>> Bye
>>
>> Jeff Barnett schrieb:
>>> On 11/30/2025 5:36 AM, Mild Shock wrote:
>>>> Hi,
>>>>
>>>> What we thought:
>>>>
>>>> Prediction 5 . It will never be proved that
>>>> Σ(5) = 4,098 and S(5) = 47,176,870.
>>>> -- Allen H. Brady, 1990  .
>>>>
>>>> How it started:
>>>>
>>>> To investigate AlphaEvolve’s breadth, we applied
>>>> the system to over 50 open problems in mathematical
>>>> analysis, geometry, combinatorics and number theory.
>>>> The system’s flexibility enabled us to set up most
>>>> experiments in a matter of hours. In roughly 75% of
>>>> cases, it rediscovered state-of-the-art solutions, to
>>>> the best of our knowledge.
>>>> https://deepmind.google/blog/alphaevolve-a-gemini-powered-coding-agent- 
>>>> for-designing-advanced-algorithms/
>>>>
>>>> How its going:
>>>>
>>>> We prove that S(5) = 47, 176, 870 using the Coq proof
>>>> assistant. The Busy Beaver value S(n) is the maximum
>>>> number of steps that an n-state 2-symbol Turing machine
>>>> can perform from the all-zero tape before halting, and
>>>> S was historically introduced by Tibor Radó in 1962 as
>>>> one of the simplest examples of an uncomputable function.
>>>> The proof enumerates 181,385,789 Turing machines with 5
>>>> states and, for each machine, decides whether it halts or
>>>> not. Our result marks the first determination of a new
>>>> Busy Beaver value in over 40 years and the first Busy
>>>> Beaver value ever to be formally verified, attesting to the
>>>> effectiveness of massively collaborative online research
>>>> https://arxiv.org/pdf/2509.12337
>>>>
>>>> They claim not having used much AI. But could for
>>>> example AlphaEvolve do it somehow nevertheless, more or
>>>> less autonomously, and find the sixth busy beaver?
>>> I'm fascinated by this result and I'd appreciate it if you could 
>>> elaborate more. Is the problem presented to the automation:
>>>
>>>   1. Prove "S(5) = 47,176,870" along with a 'def' of S?
>>>   2. Enumerate & check behavior or 47,176,870 machines?
>>>   3. Like 2 above but supplied with lemmas such as prove this case halts
>>>      implies a large number of other cases halt faster?
>>>   4. Like 3 above but lemmas discovered, perhaps with 'encouragement'?
>>>   5. other approaches or other chore splits between man and machine?
>>>   6. etc?
>>>
>>> I think what I'm asking is for the work flow that led to the result.
>>
>

Back to comp.lang.prolog | Previous | Next — Previous in thread | Find similar | Unroll thread

Thread

Could AlphaEvolve find the sixth busy beaver ? Mild Shock <janburse@fastmail.fm> - 2025-11-30 13:36 +0100
  An old Busy Beaver ASIC (Application-Specific Integrated Circuit) (Re: Could AlphaEvolve find the sixth busy beaver ?) Mild Shock <janburse@fastmail.fm> - 2025-11-30 13:56 +0100
  Re: Could AlphaEvolve find the sixth busy beaver ? Jeff Barnett <jbb@notatt.com> - 2025-12-01 14:29 -0700
    Re: Could AlphaEvolve find the sixth busy beaver ? Mild Shock <janburse@fastmail.fm> - 2025-12-02 00:14 +0100
      FYI: The Busy Beaver Frontier / Scott Aaronson (Was: Could AlphaEvolve find the sixth busy beaver ?) Mild Shock <janburse@fastmail.fm> - 2025-12-02 00:17 +0100
        2024 claim of BB(5) (Was: FYI: The Busy Beaver Frontier / Scott Aaronson ) Mild Shock <janburse@fastmail.fm> - 2025-12-02 00:22 +0100

csiph-web