Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > sci.math > #641484 > unrolled thread

Could AlphaEvolve find the sixth busy beaver ?

Back to article view | Back to sci.math

Contents

  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

#641484 — Could AlphaEvolve find the sixth busy beaver ?

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?

Bye

[toc] | [next] | [standalone]

#641485 — An old Busy Beaver ASIC (Application-Specific Integrated Circuit) (Re: Could AlphaEvolve find the sixth busy beaver ?)

Hi,

Wonder why the Coq proof even should be
different from anything that AI could produce.
Its not a typical Euclid proof in a few steps,

it rather uses also enumeration, just like the
Fly Speck proof, for the Keppler Conjecture. So
lets see what happens next, could AlphaEvolve

find the sixth busy beaver?

Bye

P.S.: Here picture of an old Busy Beaver ASIC
(Application-Specific Integrated Circuit)

Application    Fun
Technology    1500
Manufacturer    VLSI Tech
Type    Semester Thesis
Package    DIP64
Dimensions    3200μm x 3200μm
Gates    2 kGE
Voltage    5 V
Clock    20 MHz

The Busy Beaver Coprocessor has been designed to solve the Busy Beaver 
Function for 5 states. This function (also known as the Rado's Sigma 
Function) is an uncomputable problem from information theory. The input 
argument is a natural number 'n' that represents the complexity of an 
algorithm described as a Turing Machine.
http://asic.ethz.ch/cg/1990/Busy_Beaver.html


Mild Shock schrieb:
> 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?
> 
> Bye

[toc] | [prev] | [next] | [standalone]

#641538

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.
-- 
Jeff Barnett

[toc] | [prev] | [next] | [standalone]

#641547

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.

[toc] | [prev] | [next] | [standalone]

#641548 — FYI: The Busy Beaver Frontier / Scott Aaronson (Was: Could AlphaEvolve find the sixth busy beaver ?)

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

[toc] | [prev] | [next] | [standalone]

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

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

[toc] | [prev] | [standalone]

Back to top | Article view | sci.math

csiph-web