I should add that this mathematical discovery would not have been possible without Coq, a computer program that checks proofs for errors.
The Coq Proof Assistant <https://coq.inria.fr/> John K Clark See what's on my new list at Extropolis <https://groups.google.com/g/extropolis> On Tue, Jul 2, 2024 at 1:34 PM John Clark <[email protected]> wrote: > There are well defined finite integers that cannot be calculated, for > example the Busy Beaver function produces them because at some point it > grows faster than stacked exponentials or the Ackermann function or any > other computable sequence. The Busy Beaver is a N state Turing Machine > which starts with an all zero tape, and BB(N) is defined as the largest > FINITE number of 1's printed on the tape AFTER it halts. Some Turing > Machines never halt and just keep printing 1's forever but they don't > count, it must halt. > > We've known the first 4 Busy Beaver numbers for about 40 years, they are: > BB(1)=1 > BB(2)=4 > BB(3) =6 > BB(4)=13 > and as of today we also know the fifth > BB (5) = 2098 > > Nobody knows what BB(6) is and probably nobody will ever know, but we do > know that it's larger than 10^10^10^10^10^10^10^10^10^10^10^10^10^10^10. > > A related concept called S(n) is the number of moves an n State Turing > machine makes before it halts. Here are the correct values for the first 5 > busy beaver machines that halt: > s(1) = 1 move > S(2) = 6 moves > S(3) = 21 moves > S(4) = 107 moves > S(5) = 47,176,870 moves > > With Fifth Busy Beaver, Researchers Approach Computation’s Limits > <https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702> > > John K Clark See what's on my new list at Extropolis > <https://groups.google.com/g/extropolis> > > oml > > > -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/CAJPayv0S3nfCnUuKvcTjrFShQVELbYqbAfiUPpXCav6onYTFQA%40mail.gmail.com.
