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

Groups > comp.lang.prolog > #15067

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

Cross-posted to 3 groups.

Show all headers | View raw

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

Back to comp.lang.prolog | 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