Computabillity of packing of spheres with different radii This is a conceptually easier version of a box packing problem I stated earlier.
Let $n$ be a positive integer and let $r_1, \ldots, r_n$ be positive integers. We take $r_i$ to be the radius of a sphere in $\mathbb{R}^3$ for each $i\in \{1,\ldots, n\}$.
Let $R$ be the minimum positive integer such that we can pack all the small spheres into one big sphere of radius $R$.
Is the problem of finding $R$ given $n$ and the radii $\{r_i:i\in\{1,\ldots, n\}\}$ of the small spheres, computable?
 A: Yes, it is computable.  Use the decidability of the theory of the real numbers $(\mathbb{R}, 0, 1, \times, +, <)$.  With a very little standard work, you can define $\mathbb{R}^3$, vector addition, and the norm function $|x|$. Then using the decidability of real-closed fields search for the minimum $R \in \mathbb{N}$ such that the following is true:
$$ \exists x_0, ..., x_n \in \mathbb{R}^3 \left(\bigwedge_{i \neq j} |x_i - x_j| \geq r_i + r_j \quad \land\quad \bigwedge_{i}|x_i| + r_i \leq R\right) $$
This search will terminate before $R > r_1 + ... + r_n$.

If you relax it to reals, then it is also computable.  First, we can fit the balls within a large sphere of center the origin and radius $R' = r_1 + ... + r_n$ by lining the balls in a line. 
Then you can use compactness.  The function $R(x_1, ..., x_n) = \min_i (|x_i| + r_i)$ is computable and it describes the minimal radius $R$ which fits all the balls if they have center $x_i \in \mathbb{R}^3$.  Now the desired value $R$ is equal to $\inf_{x_1, ..., x_n} R(x_1, ..., x_n)$ where the minimum is over all $x_i, x_j$ such that $|x_i| \leq R'$ and $|x_i - x_j| \geq r_i + r_j$.  Classically, this this is an infimum over a continuous function on a compact domain so it is realized.  Computably, this minimum is also computable since it is the minimum of a computable function whose domain is what is called a "computable subset of $\mathbb{R}^3$" in the computable analysis literature.
