From Newsgroup: comp.lang.prolog

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

--- Synchronet 3.21a-Linux NewsLink 1.2