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
Hi,I'm fascinated by this result and I'd appreciate it if you could
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?
On 11/30/2025 5:36 AM, Mild Shock wrote:
Hi,I'm fascinated by this result and I'd appreciate it if you could
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?
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.
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,I'm fascinated by this result and I'd appreciate it if you could
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?
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.
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,I'm fascinated by this result and I'd appreciate it if you could
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?
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.
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,090 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 158:12:45 |
| Calls: | 13,922 |
| Files: | 187,021 |
| D/L today: |
221 files (58,560K bytes) |
| Messages: | 2,457,273 |