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

Groups > sci.math > #641548

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

Cross-posted to 3 groups.

Show all headers | View raw

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 sci.math | Previous | Next — Previous in thread | Next 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