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