XPost: sci.physics, comp.theory   
   From: janburse@fastmail.fm   
      
   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-cod   
   ng-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)