[HN Gopher] With fifth busy beaver, researchers approach computa...
___________________________________________________________________
With fifth busy beaver, researchers approach computation's limits
Author : LegionMammal978
Score : 259 points
Date : 2024-07-02 14:27 UTC (8 hours ago)
(HTM) web link (www.quantamagazine.org)
(TXT) w3m dump (www.quantamagazine.org)
| jl6 wrote:
| BB(0) = 0
|
| BB(1) = 1
|
| BB(2) = 4
|
| BB(3) = 6
|
| BB(4) = 13
|
| They just proved that BB(5) = 47,176,870.
|
| It is known that BB(6) must be at least 10^10^...^10 (a tower of
| exponents fifteen levels high).
|
| https://en.wikipedia.org/wiki/Busy_beaver#Known_values_for_%...
| pdonis wrote:
| The definitions of the "BB" function don't all appear to be the
| same. The article referenced in this overall discussion says
| BB(2) = 6. In the notation of the Wikipedia article you
| reference, this would be S(2) = 6; S is the number of steps.
| What has now been proved is that S(5) = 47,176,870.
|
| However, your BB values for 0, 1, 2, 3, and 4 match the
| Wikipedia article's notation for Sigma; Sigma is the number of
| 1s written on the tape at halting. In that notation, what has
| now been proved is Sigma(5) = 4098.
| LegionMammal978 wrote:
| Yeah, this is a bit confusing, and the subject of repeated
| internal controversy. Most of the twentieth-century authors
| focused on the number of 1s, S( _n_ ), following Rado's
| original practice of treating s(M) as the score of a machine
| M in the "Busy Beaver game". But when Aaronson re-popularized
| it in 2020 [0], he used BB( _n_ ) to denote the number of
| steps (which Rado called S( _n_ )), and the bbchallenge
| project has been using this latter convention for publicity.
| Pascal Michel's website [1] has all the S( _n_ ) and S( _n_ )
| bounds up to _n_ = 7.
|
| Personally, I think both functions have their strengths and
| weaknesses. S( _n_ ) is easier to calculate for machines that
| run too long to be simulated directly (e.g., Skelet #1 from
| the article) but leave a known pattern on the tape, and it
| also has historical priority. But S( _n_ ) has a simpler
| argument for being undecidable, since it provides a trivial
| filter for testing if a candidate machine cannot halt. Also,
| s(M) is a bit weird in that it has no lower bound in terms of
| s(M), since an adversarial machine could do a colossal amount
| of work before wiping its tape at the end.
|
| Regardless, past BB(3), there isn't any known size where the
| champion machines for S( _n_ ) and S( _n_ ) are different.
| (At least, the _sets_ of champion machines aren 't disjoint:
| S(5) = 4098 is shared by both the S(5) champion and another
| machine that runs a quarter as long.) The score of a machine
| is dominated by googological strength rather than
| technicalities in the definition.
|
| [0] https://scottaaronson.blog/?p=4916
|
| [1] https://bbchallenge.org/~pascal.michel/ha
| pdonis wrote:
| Thanks for this information, it's very helpful! Also I had
| no idea that "googological strength" was a thing. :-)
| Sharlin wrote:
| I'll just leave this here:
| https://googology.fandom.com/wiki/Googology_Wiki
| nickdrozd wrote:
| > past BB(3), there isn't any known size where the champion
| machines for S(n) and S(n) are different.
|
| My feeling is that this trend cannot continue forever, and
| for infinitely many N they are different. If they are
| always the same, then you could find the steps champion
| just by finding the marks champion. This would be
| convenient, because as you pointed out, steps are more
| logically important, while marks are more practically
| important. But this feels too good to be true, and so it
| probably isn't.
| LegionMammal978 wrote:
| Hmm, around _n_ = 2 or _k_ = 2, there are only 2 added
| transitions for a machine to do "the next big thing"
| googologically, so that doesn't leave much slack for many
| different machines at the same level. But maybe that
| could happen closer to the _n_ = _k_ line, where each
| increment adds many new transitions. Or to the contrary,
| maybe each increment just does several "next big
| things".
| Natsu wrote:
| Looking at the pictures on Wikipedia regarding those programs,
| it's interesting how they seem to result in fractals.
| LegionMammal978 wrote:
| This mainly has to do with the BB(5) champion having
| "bouncing" behavior: it moves from the left side of the
| current pattern to the right side and back again, each time
| extending it slightly. Since the time it takes to grow the
| pattern is strictly proportional to its current size, you end
| up with a bunch of parabolas that appear self-similar.
| jerf wrote:
| That is because these are small. Small machines can not help
| but still have those sorts of patterns in them. See all the
| simple 1-D automata of interest, for instance:
| https://atlas.wolfram.com/01/01/
|
| As you step up I am fairly confident you'll see the winners
| get noisier and noisier. They'll have some sort of pattern,
| just ones you won't be able to comprehend. For some suitable
| definition of "noisier" this might even be a provable claim.
| Natsu wrote:
| Wouldn't it make more sense for the longest running ones to
| be fractal in a sense given that the self-similarity is
| sort of compressible? I guess we'll probably never know,
| because it's not clear that we'll ever find another BB
| winner.
| kryptiskt wrote:
| One notable thing here is that the proof is a Coq proof. I wonder
| if it is the first significant proof that starts out implemented
| in a theorem prover, instead of being a known proof translated to
| such a system.
|
| Note that there have been computer-assisted proofs before (four-
| color theorem, Kepler's conjecture), but those were not done in a
| formally verified setting until later.
| LegionMammal978 wrote:
| As far as I am aware, all of the proofs and techniques for each
| machine were present before mxdys managed to get the whole
| theorem into Coq: the main problem was that the deciders and
| manual proofs were disorganized and somewhat suspect. The worst
| offenders here were Skelet #1, which needed a bespoke program
| to accelerate it to its ultimate pattern [0], and Skelet #17,
| which took Xu seven pages' worth of dense reasoning to prove
| non-halting [1]. The full Coq proof put a much-needed degree of
| confidence into these results.
|
| [0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html
|
| [1] https://discuss.bbchallenge.org/t/skelet-17-does-not-
| halt/18...
| poikroequ wrote:
| > [The four color theorem] was the first major theorem to be
| proved using a computer.
|
| https://en.m.wikipedia.org/wiki/Four_color_theorem
|
| I guess maybe I don't understand what you mean by "formally
| verified setting", but I believe the four color theorem was
| first proven using a computer.
|
| > Although flawed, Kempe's original purported proof of the four
| color theorem provided some of the basic tools later used to
| prove it.
|
| It sounds like Kempe laid some of the groundwork, but then the
| theorem was ultimately proved using a computer.
|
| I could be wrong though, I'm not an expert in this area.
| nyssos wrote:
| The original four color theorem proof used a computer as a
| computational aid for some nasty casework: the procedure for
| checking each case and the list of cases that needed to be
| checked were found by hand.
|
| Proving something in a theorem prover means the proof itself
| is an object constructed in the prover's language.
| Almondsetat wrote:
| I think that's a bit too harsh. An entire complicated proof
| concocted solely looking at a computer screen in Coq? Every
| mathematician will have plenty of hand written sketches,
| ideas and parts of proofs. Does that mean it was "ported"
| to Coq?
| Sniffnoy wrote:
| > I think that's a bit too harsh. An entire complicated
| proof concocted solely looking at a computer screen in
| Coq?
|
| Nobody is suggesting this, and in this case, it was
| indeed "ported" to Coq from existing sketches.
|
| The distinction here isn't between on-paper-first vs
| computer-first. The distinction here is between using a
| custom computer program to perform computations for a
| mostly-paper proof, versus taking an existing general-
| purpose theorem-checker (Coq, in this case) and writing
| down the entire proof in its language so it can check it.
| MaxBarraclough wrote:
| I'm no expert either, but it's interesting to note that the
| original computer-aided proof was erroneous. ctrl-f for
| _Schmidt_ on the Wikipedia page.
| ks2048 wrote:
| Apparently, this is the proof in 19,000 lines of Coq:
| https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v
| bryan0 wrote:
| Aaronson's post on BB(5): https://scottaaronson.blog/?p=8088
| pvg wrote:
| Some comments on this result by Scott Aaronson
| https://scottaaronson.blog/?p=8088
|
| And for leisure-class beavers, some big related threads from
| earlier this year:
|
| https://news.ycombinator.com/item?id=40453221
|
| https://news.ycombinator.com/item?id=38113792
|
| https://news.ycombinator.com/item?id=37910297
| inhumantsar wrote:
| > leisure-class beavers
|
| I can't not find this phrase funny. out of context it reads
| like something out of Terry Pratchett or Douglas Adams.
| phaedrus wrote:
| I wrote program to solve the cutting stock problem
| (https://en.wikipedia.org/wiki/Cutting_stock_problem) for a
| personal project. I couldn't (or didn't want to) use any existing
| program for it because my stock involved cutting pieces shaped
| like either /---/, /---|, or |---| and I didn't want to waste
| material on the 45 cut.
|
| I find it interesting that the description of Brady's program to
| optimize search for BB(4) by cutting out search subtrees whose
| differences don't matter is fairly close to a description of what
| I did to make my program fast.
| wodenokoto wrote:
| So we were just lucky that all non-halting programs of length 5
| just happened to be provably non-halting?
| tromp wrote:
| The article touches on that:
|
| > But just four days ago, mxdys and another contributor known
| as Racheline discovered a barrier for BB(6) that seems
| insurmountable: a six-rule machine whose halting problem
| resembles a famously intractable math problem called the
| Collatz conjecture. Connections between Turing machines and the
| Collatz conjecture date back to a 1993 paper by the
| mathematician Pascal Michel, but the newly discovered machine,
| dubbed "Antihydra," is the smallest one that appears unsolvable
| without a conceptual breakthrough in mathematics.
| dwh452 wrote:
| I'm curious how the Turing machines can resemble problems
| which take input? BB(n) is defined as a n-state Turing
| machine that starts off with an empty tape. Collatz(n) is how
| many steps are taken before it terminates when starting with
| input 'n'.
|
| Does this mean a BB(6) machine which resembles Collatz is
| testing all possible values as part of it program and not
| part of anything on the tape (since the tape start out
| empty)?
| LegionMammal978 wrote:
| It's not testing all values, but one particular starting
| point. In all likelyhood, it will never reach its stopping
| condition from this starting point, but proving this even
| for a single value is currently intractable. Compare with
| the "5 _x_ + 1 " variant of the Collatz cojecture, where
| many values are believed (but not proven) to run off to
| infinity, never to return.
| LegionMammal978 wrote:
| Yes. In fact, Allen Brady feared as early as 1988 that there
| would be a totally intractable machine with 5 states [0]:
|
| > _Prediction 5._ It will never be proved that S(5) = 1,915 and
| _S_ (5) = 2,358,064. (Or, if any larger lower bounds are ever
| found, the new values may be substituted into the prediction.)
|
| > Reason: Nature has probably embedded among the five-state
| holdout machines one or more problems as illusive as the
| _Goldbach Conjecture_. Or, in other terms, there will likely be
| nonstopping recursive patterns which are beyond our powers of
| recognition.
|
| Luckily, this prediction did not come to pass, but only by a
| margin of one extra state.
|
| [0] Allen Brady, "The Busy Beaver Game and the Meaning of
| Life", in Rolf Herken (ed.), _The Universal Turing Machine: A
| Half-Century Survey_ , Oxford University Press, 1988, pp.
| 259-277. This chapter can also be found in the 2nd ed.,
| Springer, 1995, pp. 237-254.
| Sniffnoy wrote:
| When you say "provably", do you mean that in the mathematical
| sense or in a practical sense?
|
| For the practical sense, other commenters have already replied.
|
| For the mathematical sense, I would say it would be pretty
| surprising to me if BB(5) had been undecidable -- 5 states and
| 2 symbols is just so few with which to try to encode
| undecidable behavior.
|
| However, it's worth noting that as a consequence of the
| incompleteness theorem, there must be _some_ n such that
| standard mathematics cannot prove the value of BB(n). And in
| recent years various people have been working on finding such n
| and seeing how low they can get the number. The current
| record[0] is 745.
|
| I expect that record can be probably be brought lower (more
| easily than the record for computing BB can be brought
| higher!), but even so, that's a lot of distance between 5 (the
| highest we know) and 745 (the lowest we know to be unknowable).
|
| [0]This is the current record both for ZFC and for PA, in case
| you're wondering what I mean by "standard mathematics"... so it
| at least ought to be possible to bring it down further for PA!
| I think so far nobody's found a way to do better for PA than
| for ZFC, even though, like, that has to be possible, right?
| ko27 wrote:
| Are there any interesting mathematical problems that can be
| encoded with 5 states and 2 symbols, which now we can prove
| using BB(5)?
| Sniffnoy wrote:
| I don't believe so. But even if there were, unfortunately,
| these things basically work the other way around.
|
| If you can encode a problem in n states, and you know
| BB(n), then, as you say, you could use that to solve the
| problem. Trouble is, how do you know BB(n)? In reality, the
| only way to determine BB(n) is to go and solve all such
| problems; there isn't any other easier method that you can
| apply that would then let you get answers for these
| problems as a consequence.
|
| So, the value of BB(n) will always be a summation of "we
| did all the hard work of solving all the n-state problems",
| not something you do separately to get those answers out.
| UncombedCoconut wrote:
| Mostly no: we did find some non-halting TMs that required
| new proofs, but none of those had the flavor of new math,
| per se. Indeed, we found that all but 30 of them could be
| proved by finite automata methods, meaning the TM's
| state/tape at any step could be reduced to one of finitely
| many states and we'd still know all we needed to know about
| future steps. I would argue that such a non-halting proof
| can't have much mathematical content. (Maybe a bit, in
| about the same way that an integer equation is sometimes
| proved unsolvable by considering it modulo n and checking
| every case.) Also, I learned some math I wasn't personally
| familiar with from the analysis of a particular machine:
| https://www.sligocki.com/2023/03/14/skelet-10.html
| (Zeckendorf's Theorem).
| tromp wrote:
| > There are many variants of the original busy beaver problem,
| and some Busy Beaver Challenge contributors plan to keep working
| on these.
|
| One such variant is a functional busy beaver defined in terms of
| the lambda calculus [1]. Since it measures program size in bits
| rather than states, it allows many more values to be determined
| (37 so far versus only 6 for TMs), and the gap between the
| largest known value and values beyond Graham's Number is a mere
| 13 program bits. A closely related variant [2] can be directly
| expressed in terms of Kolmogorov complexity, which Mikhail
| Andreev argues [3] is crucial for applications in Information
| Theory.
|
| [1] https://oeis.org/A333479
|
| [2] https://oeis.org/A361211
|
| [3] https://arxiv.org/pdf/1703.05170
| passion__desire wrote:
| Isn't there another formulation of BB where we count shifts
| (from left to right, and from right to left) a TM makes instead
| of strings of contiguous 1s. I remember seeing a video about
| this definition.
| Sniffnoy wrote:
| The variant of BB discussed in the article is counting steps,
| not 1s. (I guess "shifts" is equivalent to steps, although
| that seems like a more roundabout way of specifying it.)
| Also, I don't think anyone counts strings of _contiguous_ 1s,
| although of course one could define such a thing.
| titanomachy wrote:
| I worked for a couple years with a formidable and
| incomprehensibly smart engineer who ascended the IC ranks faster
| than anyone I've seen at an elite tech company. He quit the job a
| few years ago, and when I asked him his plans he told me he was
| going to work on the busy beaver problem. I can't help but wonder
| if he is mxdys, the pseudonymous contributor mentioned in the
| article who wrapped up the formal proof of BB(5). I'll probably
| never know.
| jebarker wrote:
| If it were them would you be surprised that they wanted to
| remain anonymous?
| danavar wrote:
| A message on LinkedIn or email never hurt!
| ks2048 wrote:
| According to Scott Aaronson's blog post on this, there are
| 16,679,880,978,201 5-state Turing machines. I wonder if we know
| what percentage of them halt?
|
| Edit: number of TM for n states: (4n + 1)^(2n). Found this (for
| smaller n), which is the kind of analysis I was curious about:
| https://github.com/LukasKalbertodt/beaver
| nayuki wrote:
| From the article:
|
| > To distill the essence of the halting problem into a simpler
| form, Rado imagined sorting Turing machines into groups based on
| how many rules they had -- one group for all one-rule Turing
| machines, another for all two-rule machines, and so on. Sure,
| that leaves infinitely many such groups, since a Turing machine
| can have any number of rules. But the number of distinct machines
| in every group is finite, since there are only so many possible
| combinations of rules.
|
| > With two rules, there are already over 6,000 distinct Turing
| machines to consider; that number swells to millions with three
| rules, and to billions with four.
|
| I'm pretty sure the standard terminology is "states", not
| "rules". This deviation made it harder to understand.
|
| Each state produces 2 transition rules, depending on the symbol
| at the tape head.
| smokel wrote:
| The original Busy Beaver paper by Tibor Rado ("On Non-Computable
| Functions") is actually quite easy and fun to read.
|
| For a modern version of the paper with some additional notes, see
| https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
| nickdrozd wrote:
| Congratulations to the team! So the (blank tape) halting problem
| is solved for 5-state 2-color Turing machine programs. Has anyone
| tried applying these same techniques to the 2-state 4-color case?
| That seems like it would probably be tractable, although
| generally speaking colors are more powerful than states, so there
| might be some surprises there. (6-state 2-color and 2-state
| 5-color both seem intractable, perhaps even provably so.)
|
| By the way, there is an extremely stupid but disturbingly
| widespread idea that humans are able to just intuit solutions to
| the halting problem, using the mind's eye or quantum mechanics in
| the brain or whatever. Needless to say, this did not factor into
| the proof.
| tromp wrote:
| > the 2-color 4-state case?
|
| You mean the 2-state 4-color case...
| nickdrozd wrote:
| Fixed, thanks
| LegionMammal978 wrote:
| > Has anyone tried applying these same techniques to the
| 2-color 4-state case?
|
| I assume you mean the 4-color case. As I understand it, the
| deciders currently in use are sufficient to prove all the 2x4
| holdouts non-halting. So the current champion gives us S(2,4) =
| 2,050 and S(2,4) = 3,932,964, barring some big errors in the
| decider design. The result just hasn't been organized in one
| place.
|
| > (6-state 2-color and 2-state 5-color both seem intractable,
| perhaps even provably so.)
|
| Yes, 2x5 has the Hydra, and 6x2 has the Antihydra, which
| compute the same iteration, but with different starting points
| and halting conditions. The standard conjecture (related to
| Mahler's 3/2 problem) is that this iteration is uniformly
| distributed mod 2, and a proof of that conjecture would very
| likely prove both machines non-halting, by yielding suprema and
| infima on the cumulative ratio of 0s to 1s. But of course there
| is no known method of proof.
| srcreigh wrote:
| > By the way, there is an extremely stupid but disturbingly
| widespread idea that humans are able to just intuit solutions
| to the halting problem, using the mind's eye or quantum
| mechanics in the brain or whatever. Needless to say, this did
| not factor into the proof.
|
| The year is 52,000 CE and humans have solved BB(18) in the
| sense of exhaustively categorizing halting vs non-halting
| 19-state no-input programs. They have used a proof generator
| based on a logical theory called Aleph*, and at that time it
| had been known for 1.5k years that ZFC is incapable of
| establishing BB(18).
|
| Compared to the year 2024 CE, considerable millennia before
| Aleph* came into use, it is clear that no program written at
| that point in history was capable of even using brute force
| proof checking to solve BB(18) in theory (like how we can
| enumerate and check ZFC proofs today to solve BB(??) in
| theory).
|
| That's what is meant by the "humans intuit solutions to the
| halting problem" position. AFAIK, there's no known hard,
| theoretical reason why the above laid out future history cannot
| take place. And due to BB being incomputable, humans had to
| develop new theory to be able to construct the programs
| required. _Something_ has to be accredited for the results, and
| it can 't be computation since the programs did not exist.
| LegionMammal978 wrote:
| > AFAIK, there's no known hard, theoretical reason why the
| above laid out future history cannot take place.
|
| Probably the biggest issue is that they'd have no method to
| establish that Aleph* is consistent. To continue this BB
| chain indefinitely, you must invent further and further
| first-order theories, each of which might not be consistent,
| let alone S1-sound. And with an S1-unsound theory, any
| halting proof might not hold up in the standard model of the
| integers. You'd effectively have to postulate an indefinite
| amount of oracular knowledge.
|
| Also, another physical issue: you can show that within any
| consistent, recursively axiomatizable theory, the length of
| the shortest proof of "the longest-running _n_ -state machine
| is M" must grow at an uncomputable rate in terms of _n_.
| Ditto for the shortest proof of "machine M halts", where M
| is factually the longest-running _n_ -state machine.
| Otherwise, a machine could use a computable bound on the
| proof length to solve the halting problem. Therefore, the
| proof should very quickly become too large to fit within our
| light cone.
|
| In any case, the BB-related evidence for that position rested
| on BB(5) being determinable by extending the techniques used
| for BB(4). But in fact, it turns out that similar extensions
| don't even get you to BB(6). So there isn't anything to
| support the position, other than the pure speculation that
| anything is physically achievable given enough time.
| srcreigh wrote:
| Thanks for sharing interesting info!
|
| How do we know that there would be consistency issues or
| S1-soundness issues?
|
| Your claim about proof size categorizing n-state machine
| halting status is new to me. Do you have any links to read
| more about this?
|
| The argument doesn't make sense to me. Rather it seems like
| more of a consequence of BB being incomputable in the first
| place. The proof sizes for each BB(n) aren't expected to be
| computable at all. There is necessarily a different theory
| for each n (or intervals of n where each theory applies
| with limits on each).
|
| > So there isn't anything to support the position, other
| than the pure speculation that anything is physically
| achievable given enough time.
|
| Something something burden of proof something. It would be
| extremely fascinating to have a conclusive argument that
| large BB numbers cannot be solved.
| LegionMammal978 wrote:
| > How do we know that there would be consistency issues
| or S1-soundness issues?
|
| From Godel's second incompleteness theorem, no consistent
| first-order recursively-axiomatizable theory (i.e., a
| theory that can have its proofs validated by a Turing
| machine) can prove its own consistency. Thus, to prove
| that your current theory (e.g., ZFC) is consistent, you
| must move to a stronger one (e.g., Aleph*). But then you
| can't prove the consistency of that without an even
| stronger theory, and so on. Thus, you end up with an
| infinite regression, and you can't ultimately prove the
| consistency of any of these theories.
|
| > Your claim about proof size categorizing n-state
| machine halting status is new to me. Do you have any
| links to read more about this?
|
| Not really, other than some of my own ramblings on the
| bbchallenge Discord server. But it's not that long:
|
| Suppose that the longest-running _n_ -state machine M can
| always be proven to halt using a proof of under f( _n_ )
| symbols, where f( _n_ ) is some fixed computable
| function. Then, you could construct a TM that, given _n_
| , enumerates every valid proof of length less than f( _n_
| ) symbols, and checks whether it shows that a particular
| _n_ -state machine halts. The TM then simulates all of
| the proven halters to see how long they run. By
| assumption, the longest-running machine M is included in
| this list. So this TM can compute BB( _n_ ), which is an
| impossibility. Therefore, the function f( _n_ ) cannot
| exist.
|
| As a corollary, since it's "uncomputably difficult" to
| prove that the longest-running machine halts at all, it's
| no less difficult to fully establish the value of BB( _n_
| ).
| srcreigh wrote:
| > Thus, you end up with an infinite regression, and you
| can't ultimately prove the consistency of any of these
| theories.
|
| There is similar issue with even ZFC and PA. It's not
| really a dealbreaker imo.
|
| > Suppose that the longest-running n-state machine M can
| always be proven to halt using a proof of under f(n)
| symbols, where f(n) is some fixed computable function.
| Then, you could construct a TM that, given n, enumerates
| every valid proof of length less than f(n) symbols
|
| The issue with that argument is that the TM which
| enumerates every valid proof can't exist in the first
| place.
|
| If you fix an axiomatic theory, it's already known that
| the theory has a limit.[1]
|
| If every theory has a limit, you need countably
| infinitely many axiomatic theories together to prove
| BB(n) for all n. So there's no TM which can even
| enumerate all the proofs, since a TM must have finite
| states, and thus can't enumerate infinitely many proof
| systems.
|
| (In fact for similar reasons I believe a Halt program,
| which has infinite states but which works for all TMs
| with finite states, platonically exists. It's an emulator
| and an infinitely long busy beaver number lookup table.
| The diagonalization argument doesn't apply, since the
| infinite Halt doesn't accept itself as input.
|
| This Halt would have countably many states since each
| busy beaver number is finitely calculated and there's
| only countably many of them.)
|
| So it's not clear that f(n) is uncomputable. If f(n) is
| the symbol count and not the binary encoded length of the
| symbols, it even seems that it's trivially bounded by
| some constant for all n. The proof could be one symbol
| the meaning of which is encoded in the theory.
|
| It is a fascinating question though. I'm sure there is
| some function of axiomatic theory proof checker TM size
| and binary encoded proof length which does grow with n.
| It's unclear if it would be uncomputable though.
|
| The consequence of it being uncomputable is that the
| universe doesn't have the resources to even encode the
| theory and/or represent it's proofs.
|
| In fact I suppose even as long as it grows at all, there
| would be a limit to BB(n) which can be possibly
| determined. Very fascinating
|
| [1]: page 5 https://www.scottaaronson.com/papers/bb.pdf
| nickdrozd wrote:
| > They have used a proof generator based on a logical
| theory...
|
| I don't understand your scenario. If they're using a proof
| generator, that sounds like the opposite of intuiting or
| using the human mind. Maybe they used "intuition" to come up
| with new axioms for a logical theory, but that is not the
| same as determining of some particular concrete TM program
| whether or not it halts.
| srcreigh wrote:
| You got it - the creative developments of a stronger
| theory. This allows the creation of tools which can
| categorize TMs, tools which wouldn't exist otherwise.
|
| It's fascinating that the entire space of finite amounts of
| random gibberish contains every such stronger theory.
|
| As a thought experiment it does well. Interestingly the
| Church-Turing thesis seems to exclude ingenuity. That is,
| it doesn't try to say there aren't functions on natural
| numbers which are uncomputable but can be calculated with
| ingenuity. Seems that a ton of people conflate those
| things.
| ganzuul wrote:
| > extremely stupid
|
| This is simply a test for if consciousness has infinite
| computational resources.
| wayeq wrote:
| > "After decades of uncertainty, a motley team of programmers has
| proved precisely how complicated simple computer programs can
| get."
|
| my team has also proved this via our production codebase
| kaptainscarlet wrote:
| These researchers clearly haven't looked at our NodeJS ERP
| system.
___________________________________________________________________
(page generated 2024-07-02 23:00 UTC)