Will we have a proof that an explicit 2-symbol 6-state Turing Machine is the machine that runs for BB(6) steps before halting?
Knowing the exact value of BB(6) might be challenging; it is a very large number, at least 10↑↑15. It would be impossible to write it down in normal base 10 notation. Bounds using Knuth's up-arrow notation or similar approaches might be loose bounds rather than exact values of BB(6).
For this question, all that is required is that a machine that runs for BB(6) steps be explicitly determined. The machine must be proven to halt, and proven that no other 2-symbol 6-state machine runs for longer. An explicit upper bound or exact value need not be proven.
https://en.wikipedia.org/wiki/Busy_beaver#Exact_values_and_lower_bounds
1,000People are also trading
I think there's a good case for NO in the form of Antihydra. On the one hand, it seems highly likely that this never halts, since the sequence of evens and odds feels like it acts like something of an pseudorandom number generator, making this a biased random walk. On the other hand, it seems possibly/probably impossible to prove concretely that this PRNG will never hit an extremely long sequence of odds and cause the machine to halt.
@BoltonBailey There's no such thing as "impossible to prove" in math.
The closest mathematical statement would be something like "the statement 'Antihydra never halts' is independent of ZFC". But knowing this would immediately imply 1) that Antihydra never halts (since if it halts, it does so at a finite time 2) we can create a new set of postulates ZFC+"antihydra never halts" that is valid iff ZFC is valid.
An attempt at predicting shorter-term progress:
/EvanDaniel/how-many-holdout-machines-will-ther
And whether we already know the machine:
[Deleted]