Aunque las respuestas apuntan correctamente que el valor exacto de $\text{BB}(n)$ es independiente de ZF para valores suficientemente grandes e incluso moderadamente grandes de $n$, sin embargo quería señalar que el esquema general de tu método de prueba es correcto. Este es un método legítimo de prueba.
Es decir, lo que estoy diciendo es que si de alguna manera pudiéramos conocer el verdadero valor de $\text{BB}(n)$ para ciertos valores de $n$, entonces de hecho podríamos usar ese conocimiento para determinar la veracidad de la hipótesis de Riemann y así sucesivamente, para cualquier afirmación $\Pi^0_1$ cuya verdad se sepa que es equivalente a la no finalización de una máquina de Turing con a lo sumo $n$ estados. Y de hecho para cada afirmación $\Pi^0_1$ hay una máquina de Turing, ya que simplemente se escribe el código que busca un contraejemplo, finalizando cuando se encuentra. Esta máquina se ejecuta para siempre si y solo si la afirmación es verdadera. Para muchas conjeturas clásicas, el número de estados $n$ no sería muy grande, aunque el valor de $\text{BB}(n)$ sería enorme, como mencionas.
Lo que estoy diciendo es que los teoremas se demostrarían en la teoría $\text{ZFC}+\text{BB}(n)=N$, usando el supuesto adicional sobre el valor particular de la función busy-beaver. Estarías demostrando que en cada modelo de ZFC en el que el número busy-beaver en $n$ tenga ese valor, entonces de hecho la hipótesis de Riemann sería verdadera (o falsa, dependiendo del resultado del cálculo que propones llevar a cabo).
Pero además, este mismo argumento puede tomarse como una prueba de que los valores de $\text{BB}(n)$ no pueden resolverse todos en ZFC (si es consistente) incluso para algunos valores pequeños de $n$. De hecho, el valor de $\text{BB}(n)$ para $n$ moderado ni siquiera puede ser demostrablemente acotado por números específicos, porque si pudiéramos hacer esto, con $n$ suficientemente grande para llevar a cabo tu propuesta con la oración de Rosser, por ejemplo, entonces ZF tendría que resolver la oración de Rosser, lo cual no hace.
En esencia, tu método de argumento propuesto se convierte en una prueba de que los valores de la función busy-beaver deben ser independientes de ZFC o de hecho de cualquier teoría fundacional que pudiéramos desear.
Una lata de gusanos filosófica. El método también abre un cierto debate filosófico polémico, sin embargo, sobre si de hecho existe un valor "verdadero" de $\text{BB}(n)$. Si el valor asumido de $\text{BB}(n)$ es realmente el valor verdadero, entonces obtendrás el verdadero valor para la hipótesis de Riemann y así sucesivamente. Muchos matemáticos creen firmemente que afirmaciones aritméticas de este tipo tienen un valor de verdad absoluto definitivo, ya sea que puedan demostrarse en ZF o ZFC+grandes cardenales o lo que sea. El fenómeno de independencia se ve como una consecuencia de la debilidad necesaria de nuestras teorías, en lugar de cualquier dificultad para una noción robusta de verdad.
Pero mientras tanto, según la posición filosófica conocida como pluralismo aritmético, puede que no haya ningún hecho definitivo en algunas afirmaciones aritméticas. Ya sabemos que diferentes modelos de ZFC e incluso ZFC más los axiomas de cardinales grandes más fuertes que tenemos pueden tener estructuras aritméticas no isomorfas diferentes $\mathbb{N}$, con verdades aritméticas diferentes, y no parece haber un argumento completamente satisfactorio de que la verdad aritmética sea determinada. Quizás el argumento de la categoricidad de Dedekind sea el más convincente, que muestra que existe hasta un isomorfismo una única estructura aritmética que satisface la aritmética de Dedekind, que incluye el axioma de inducción de segundo orden. Pero ya que esta teoría hace referencia a la estructura de segundo orden, esencialmente conjuntos arbitrarios de números, estaría basando la determinación de nuestro concepto de lo finito en nuestro concepto de "conjunto arbitrario de números". Pero ¿qué tan exitoso puede ser eso? Sería esencialmente circular.
