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