Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.prolog > #15089
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Newsgroups | comp.lang.prolog, sci.logic, sci.math |
| Subject | Re: Could AlphaEvolve find the sixth busy beaver ? |
| Date | 2025-12-02 00:14 +0100 |
| Message-ID | <10gl7ga$u4cc$1@solani.org> (permalink) |
| References | <10ghdp5$tg19$1@solani.org> <10gl1cc$1nhqt$1@dont-email.me> |
Cross-posted to 3 groups.
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 comp.lang.prolog | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll 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