XPost: comp.lang.prolog, sci.math   
   From: janburse@fastmail.fm   
      
   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.   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)