Groups | Search | Server Info | Login | Register

Groups > sci.physics > #894637

Attacking the Busy Beaver 5 [1989] (Re: The size of a Gödel sentence G)

From Mild Shock <janburse@fastmail.fm>
Newsgroups sci.physics, sci.physics.relativity, comp.theory
Subject Attacking the Busy Beaver 5 [1989] (Re: The size of a Gödel sentence G)
Date 2025-12-03 09:10 +0100
Message-ID <10gor9j$126he$2@solani.org> (permalink)
References <10ghds1$tg19$2@solani.org> <10goqnc$1263a$2@solani.org>

Cross-posted to 3 groups.

Show all headers | View raw

Hi,

Actually the BB(5) does also construct machines,
and does also look at the code of machines.
It has an amazing history, since the candidate

for the busiest beaver was already found in 1989:

47,176,870    4098    current BB(5), step champion
https://turbotm.de/~heiner/BB/mabu90.html

They use an amazing simple technique to speed up
their search. Realizing macro turing machines, that
encode what happens with k cells on a tape.

Plus heuristics to "prove" that a TM does not halt,
which seem to be sufficient for 5 state TMs. Plus
heuristics to bring the number of considered 5 state

TMs down, since without reduction they would be
26*10^12 many, but they needed only consider 5*10^7
many. So that after about ten days using a

33 MHz Clipper CPU they got their result.

Bye

P.S.: My estimate, with todays laptop can do
it in 2.5 hours, or maybe in 2.5 minutes if using
an AI accelerator. Not 100% sure. Wasn't even

thinking about such a modern replica of the
problem. Coq used Rust. We could use even something
else that would tap in AI accelerators, maybe

even JavaScript and run it in a browser.

Mild Shock schrieb:
> Hi,
> 
> Well then get an education. Every Gödel
> sentence G, has a size, doesn't it?
> The formal analogue of the Liar Paradox,
> 
> except it’s expressed arithmetically:
> 
> G ≡ ∀y¬Proof(y,┌G┐).
> 
> Gödel did explicitly construct a Gödel
> sentence G in his 1931 paper. He did not
> claim it was astronomically large,
> 
> nor impossible to write. Now you can do
> the encoded Liar also with Turing Machines TM:
> 
> 1. Fix a formal proof system S (e.g. PA) and
> an effective enumeration of all proofs.
> 2. Build a TM M(x) that, given a code x, searches
> for an S-proof of the formula with code a; if it finds
> M(x) halts <=> exists y Proof(y,x) (i.e. Prov(x)).
> 
> Etc.. etc..
> 
> Bye
> 
> dart200 schrieb:
>  > this shit makes me feel like i'm stuck in a mad house planet
>  >
>  > undecidability has nothing to do with computational complexity and 
> the fact we think the limit to decidability is bounded by how well we 
> can bit pack a self-referential turing machine into a proof is just 
> literal nonsense
> 
> 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 sci.physics | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Could AlphaEvolve find the sixth busy beaver ? Mild Shock <janburse@fastmail.fm> - 2025-11-30 13:38 +0100
  An old Busy Beaver ASIC (Application-Specific Integrated Circuit) (Was: Could AlphaEvolve find the sixth busy beaver ?) Mild Shock <janburse@fastmail.fm> - 2025-11-30 13:54 +0100
  An old Busy Beaver ASIC (Application-Specific Integrated Circuit) (Was: Could AlphaEvolve find the sixth busy beaver ?) Mild Shock <janburse@fastmail.fm> - 2025-11-30 13:55 +0100
    What is analog computing nowadays? (Re: An old Busy Beaver ASIC (Application-Specific Integrated Circuit) (Was: Could AlphaEvolve find the sixth busy beaver ?) Mild Shock <janburse@fastmail.fm> - 2025-12-01 11:25 +0100
      Wake-up call until everybody gets ear-bleeding (Re: What is analog computing nowadays?) Mild Shock <janburse@fastmail.fm> - 2025-12-01 12:01 +0100
        BB(745) is independent of ZFC (Was: Wake-up call until everybody gets ear-bleeding) Mild Shock <janburse@fastmail.fm> - 2025-12-01 12:07 +0100
          Write ZFC formulas on a tape (of a Turing machine) (Re: BB(745) is independent of ZFC ) Mild Shock <janburse@fastmail.fm> - 2025-12-02 17:18 +0100
            Turing machines have neurons (Re: Write ZFC formulas on a tape (of a Turing machine)) Mild Shock <janburse@fastmail.fm> - 2025-12-02 17:19 +0100
              A logical calculus in nervous activity [McCulloch & Pitts 1943] (Re: Turing machines have neurons) Mild Shock <janburse@fastmail.fm> - 2025-12-02 17:20 +0100
                Busy Beaver and Theory Consistency (Was: A logical calculus in nervous activity [McCulloch & Pitts 1943]) Mild Shock <janburse@fastmail.fm> - 2025-12-02 17:39 +0100
                Busy Beaver and Theory Consistency (Was: A logical calculus in nervous activity [McCulloch & Pitts 1943]) Mild Shock <janburse@fastmail.fm> - 2025-12-02 17:43 +0100
                Re: Busy Beaver and Theory Consistency (Was: A logical calculus in nervous activity [McCulloch & Pitts 1943]) Mild Shock <janburse@fastmail.fm> - 2025-12-02 23:18 +0100
      Re: What is analog computing nowadays? (Re: An old Busy Beaver ASIC (Application-Specific Integrated Circuit) (Was: Could AlphaEvolve find the sixth busy beaver ?) Maciej Woźniak <mlwozniak@wp.pl> - 2025-12-01 12:09 +0100
        parallel random-access machine (parallel RAM or PRAM (Was: What is analog computing nowadays?) Mild Shock <janburse@fastmail.fm> - 2025-12-01 12:15 +0100
          Re: parallel random-access machine (parallel RAM or PRAM (Was: What is analog computing nowadays?) Maciej Woźniak <mlwozniak@wp.pl> - 2025-12-01 13:23 +0100
            Nope, you can't, because of the CRCW instuction (Was: parallel random-access machine) Mild Shock <janburse@fastmail.fm> - 2025-12-01 17:12 +0100
              Algorithm introduced in Hogwild! SGD (Niu et al., 2011) (Was: Nope, you can't, because of the CRCW instuction) Mild Shock <janburse@fastmail.fm> - 2025-12-01 17:31 +0100
                PRAMs might be closer to physics: Boltzman machines, etc.. (Was: Algorithm introduced in Hogwild! SGD) Mild Shock <janburse@fastmail.fm> - 2025-12-01 18:02 +0100
              Re: Nope, you can't, because of the CRCW instuction (Was: parallel random-access machine) Maciej Woźniak <mlwozniak@wp.pl> - 2025-12-01 17:59 +0100
                PRAMs might be closer to physics: Boltzman machines, etc.. (Re: Nope, you can't, because of the CRCW instuction) Mild Shock <janburse@fastmail.fm> - 2025-12-01 18:05 +0100
                PRAMs might be closer to physics: Boltzman machines, etc.. (Re: Nope, you can't, because of the CRCW instuction) Mild Shock <janburse@fastmail.fm> - 2025-12-01 18:08 +0100
                Physics more difficult than Rasperry LED cube? (Was: PRAMs might be closer to physics: Boltzman machines, etc..) Mild Shock <janburse@fastmail.fm> - 2025-12-01 18:25 +0100
            Re: parallel random-access machine (parallel RAM or PRAM (Was: What is analog computing nowadays?) Thomas Heger <ttt_heg@web.de> - 2025-12-03 07:17 +0100
              Re: parallel random-access machine (parallel RAM or PRAM (Was: What is  analog computing nowadays?) Python <python@cccp.invalid> - 2025-12-03 06:46 +0000
              Re: parallel random-access machine (parallel RAM or PRAM) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-03 08:02 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas Heger <ttt_heg@web.de> - 2025-12-04 07:50 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Janis Papanagnou <janis_papanagnou+ng@hotmail.com> - 2025-12-04 09:57 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-06 17:02 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas Heger <ttt_heg@web.de> - 2025-12-07 10:22 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-07 10:39 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-07 10:46 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Janis Papanagnou <janis_papanagnou+ng@hotmail.com> - 2025-12-07 11:42 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Michael S <already5chosen@yahoo.com> - 2025-12-07 16:26 +0200
                Re: parallel random-access machine (parallel RAM or PRAM) Janis Papanagnou <janis_papanagnou+ng@hotmail.com> - 2025-12-08 04:25 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-08 08:51 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Michael S <already5chosen@yahoo.com> - 2025-12-08 13:58 +0200
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas Heger <ttt_heg@web.de> - 2025-12-09 09:15 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas Heger <ttt_heg@web.de> - 2025-12-08 08:21 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Janis Papanagnou <janis_papanagnou+ng@hotmail.com> - 2025-12-08 09:06 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas Heger <ttt_heg@web.de> - 2025-12-09 09:19 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-09 11:43 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas Heger <ttt_heg@web.de> - 2025-12-10 08:19 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-10 09:56 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-10 10:01 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas Heger <ttt_heg@web.de> - 2025-12-11 09:02 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-11 08:48 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-12 01:58 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-11 20:45 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-11 23:07 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-12 00:49 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) "Paul.B.Andersen" <relativity@paulba.no> - 2025-12-14 14:27 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-14 10:25 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) "Paul.B.Andersen" <relativity@paulba.no> - 2025-12-14 21:22 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-14 12:52 -0800
                I have a great idea The Starmaker <starmaker@ix.netcom.com> - 2025-12-14 13:11 -0800
                Einstein refrigerator (was: parallel random-access machine (parallel RAM or PRAM) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-15 03:00 +0100
                Re: Einstein refrigerator (was: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-14 19:46 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-14 10:27 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-14 10:58 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas Heger <ttt_heg@web.de> - 2025-12-15 07:50 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) "Paul.B.Andersen" <relativity@paulba.no> - 2025-12-15 14:05 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas Heger <ttt_heg@web.de> - 2025-12-16 08:44 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) "Paul.B.Andersen" <relativity@paulba.no> - 2025-12-16 22:58 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas Heger <ttt_heg@web.de> - 2025-12-17 08:50 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) "Paul.B.Andersen" <relativity@paulba.no> - 2025-12-17 14:00 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-17 10:49 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-17 11:23 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) "Paul.B.Andersen" <relativity@paulba.no> - 2025-12-17 14:24 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-18 22:13 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) The Starmaker <starmaker@ix.netcom.com> - 2025-12-19 12:02 -0800
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-17 18:24 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) John Hasler <john@sugarbit.com> - 2025-12-17 11:58 -0600
                Re: parallel random-access machine (parallel RAM or PRAM) Maciej Woźniak <mlwozniak@wp.pl> - 2025-12-12 07:19 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) "Paul B. Andersen" <relativity@paulba.no> - 2025-12-12 11:35 +0100
                Re: parallel random-access machine (parallel RAM or PRAM) Lawrence D’Oliveiro <ldo@nz.invalid> - 2025-12-18 06:49 +0000
                Re: parallel random-access machine (parallel RAM or PRAM) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-06 05:30 +0100
  Re: Could AlphaEvolve find the sixth busy beaver ? Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-11-30 14:06 +0100
    You shouldn't use NPM hacked services (Was: Could AlphaEvolve find the sixth busy beaver ?) Mild Shock <janburse@fastmail.fm> - 2025-11-30 22:27 +0100
      Its a subconscious hypothesis (Was: You shouldn't use NPM hacked services) Mild Shock <janburse@fastmail.fm> - 2025-11-30 22:33 +0100
        What if of the cosmos does a BB dance? (Was: Its a subconscious hypothesis) Mild Shock <janburse@fastmail.fm> - 2025-11-30 22:43 +0100
          Re: What if of the cosmos does a BB dance? (Was: Its a subconscious hypothesis) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-01 23:43 +0100
          Re: What if of the cosmos does a BB dance? Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-01 23:45 +0100
            newsreader where you can see the message source (Was: What if of the cosmos does a BB dance?) Mild Shock <janburse@fastmail.fm> - 2025-12-02 00:00 +0100
              Re: newsreader where you can see the message source (Was: What if of the  cosmos does a BB dance?) Python <python@cccp.invalid> - 2025-12-02 03:10 +0000
                Re: newsreader where you can see the message source (Was: What if of the cosmos does a BB dance?) Mild Shock <janburse@fastmail.fm> - 2025-12-02 11:51 +0100
                Re: newsreader where you can see the message source (Was: What if of the cosmos does a BB dance?) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-02 20:36 +0100
                Re: newsreader where you can see the message source (Was: What if of the cosmos does a BB dance?) Ross Finlayson <ross.a.finlayson@gmail.com> - 2025-12-01 21:42 -0800
                Orbits of planets in the Sol System (was: newsreader where you can see the message source) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-04 03:29 +0100
                Orbits of planets in the Sol System Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-04 03:30 +0100
              Re: newsreader where you can see the message source (Was: What if of the cosmos does a BB dance?) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-02 20:35 +0100
                Spock thinks I am interested in his gibberish (Re: newsreader where you can see the message source) Mild Shock <janburse@fastmail.fm> - 2025-12-02 23:22 +0100
                Is it like "Wirres Mückengelaber" ? (Was: Spock thinks I am interested in his gibberish) Mild Shock <janburse@fastmail.fm> - 2025-12-02 23:28 +0100
            newsreader where you can see the message source (Re: What if of the cosmos does a BB dance?) Mild Shock <janburse@fastmail.fm> - 2025-12-02 00:11 +0100
            Re: What if of the cosmos does a BB dance? Thomas Heger <ttt_heg@web.de> - 2025-12-03 07:22 +0100
              Re: What if of the cosmos does a BB dance? The Starmaker <starmaker@ix.netcom.com> - 2025-12-03 08:27 -0800
                Re: What if of the cosmos does a BB dance? Thomas Heger <ttt_heg@web.de> - 2025-12-04 07:57 +0100
        Re: Its a subconscious hypothesis (Was: You shouldn't use NPM hacked services) Maciej Woźniak <mlwozniak@wp.pl> - 2025-11-30 23:14 +0100
      Re: You shouldn't use NPM hacked services (Was: Could AlphaEvolve find the sixth busy beaver ?) Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-01 23:23 +0100
        Re: You shouldn't use NPM hacked services (Was: Could AlphaEvolve find the sixth busy beaver ?) Mild Shock <janburse@fastmail.fm> - 2025-12-02 00:05 +0100
          Re: You shouldn't use NPM hacked services Thomas 'PointedEars' Lahn <PointedEars@web.de> - 2025-12-02 20:29 +0100
    What Spock aka Thomas 'PointedEars' Lahn missed (Was: Different Hubble Theories: de Sitter Energy) Mild Shock <janburse@fastmail.fm> - 2025-12-03 01:09 +0100
  The size of a Gödel sentence G (Re: Could AlphaEvolve find the sixth busy beaver ?) Mild Shock <janburse@fastmail.fm> - 2025-12-03 09:00 +0100
  The size of a Gödel sentence G (Re: Could AlphaEvolve find the sixth busy beaver ?) Mild Shock <janburse@fastmail.fm> - 2025-12-03 09:00 +0100
    Attacking the Busy Beaver 5 [1989] (Re: The size of a Gödel sentence G) Mild Shock <janburse@fastmail.fm> - 2025-12-03 09:10 +0100
  Re: Could AlphaEvolve find the sixth busy beaver ? Sylvia Else <sylvia@email.invalid> - 2025-12-04 12:59 +0800

csiph-web