In what sense does a number "exist" if it is proven to be uncomputable?

Replying to your three mathematical/existential questions in order:

• Yes. There exists a TM that, when started on a blank tape, eventually halts (after finitely many steps) with the exact decimal expansion of $x=\Sigma\left(10^{100},10^{100}\right)$ on the tape. The same is true for $x\bmod 4$ or $x^x$ or any other natural number.
• There does not exist a natural number "that cannot be computed in any finite amount of time".
• There is no such problem for natural numbers.

On the other hand, provability is another kettle o' fish: There is no natural number $n$ such that ZFC proves $\ BB(7918)=n,$ and more recently we have that for any $m\ge 748,$ there is no natural number $n$ such that ZFC proves $BB(m)=n.$ (Here $BB$ is the Busy Beaver function w.r.t. the number of steps taken before halting.)

NB: As your questions (and your entire Intro) seemed to be about natural numbers, that is the context of my replies above. The situation is quite different in the larger context of real numbers. Note that every natural number has a finite representation, which is the basic reason it is computable. In contrast, a real number typically requires an infinite representation, which opens the possibility of not being computable. (It turns out that almost all reals are not computable.)

My view is that questions such as these arise from a failure to distinguish between intension (a description of a thing, an arithmetic expression, program source code, etc.) and extension (the thing described, the result of evaluating the expression, the observable behaviour of the compiled program, etc.). Maybe the following "theorem" will throw the difference into sharp relief.

Theorem. Every natural number is computable.

Proof. We must show that for every natural number $n$, there is a Turing machine whose output is (say) a unary representation of $n$. We proceed by induction. There is certainly a Turing machine whose output is empty, i.e. a representation of $0$. If we have a Turing machine whose output is a unary representation of $n$ it is clear that we can modify it to output just one more unit, so as to obtain a unary representation of $n + 1$. Hence every natural number is indeed computable.　◼

There is nothing wrong with the proof above, but nonetheless you may feel unable to accept the conclusion. The only way out is to conclude that there is a problem with the interpretation of the statement of the theorem. What this is actually proving is that every natural-number-in-extension is computable. This proof has nothing to do with natural-numbers-in-intension.

In order to say anything mathematically rigorous about natural-numbers-in-intension we must first choose a mathematical model for "describing natural numbers". Unfortunately, there is no canonical choice, and different choices have different expressive power. If you choose to define "description of a natural number" as "Turing machine that computes it", then tautologically every natural-number-in-intension is computable. But you could also choose to define it as "formula $\phi$ in the language of set theory with at least one free variable $n$ such that ZFC proves $\exists ! n \in \mathbb{N} . \phi$". In this case it is true that not every natural-number-in-intension is computable – or, to put it another way, there is no procedure (computable or otherwise!) that will convert the formula $\phi$ into a Turing machine that (ZFC proves) computes the unique natural number that $\phi$ describes.

I think this set of questions and direction of inquiry is one of the more interesting in philosophy and foundations of mathematics! I’ll answer your last question first: there are a variety of systems of mathematics which in various ways attempt to address the question of only allowing computable objects to exist. One good example is the subsystem of second order arithmetic $RCA_0$, which stands for the Recursive Comprehension Axiom. This axiom set is much weaker than say, Peano Arithmetic, and is one attempt at capturing the notion of “computable arithmetic”. From a computational perspective, it has many nice properties, such as the fact that any set which can be proven to exist in $RCA_0$ has a membership testing computer program, and indeed such a program can more or less be mechanically reconstructed from the proof of existence (this is more or less the Curry-Howard correspondence, see Wikipedia and this bit of Wikibooks Haskell for more).

You can also do a subset of everyday mathematics in $RCA_0$, such as proving the intermediate value theorem, the existence of algebraic closures of fields, Godel’s soundness theorem for first order logic and (a weak version of the) completeness theorem for the same. However, many mathematical statements of interest turn out not to hold in $RCA_0$, for example it is not the case that every bounded, increasing sequence of real numbers has an upper bound - precisely because there exists computable sequences of real numbers whose upper bounds are uncomputable! One example of such a sequence is a sequence of lower bounds on Chaitin's halting probability. As a result, doing mathematics in $RCA_0$ is not very nice in various ways, or at least it is a very different mathematical world than the one most pure mathematicians are used to.

For more on $RCA_0$, see for example Subsystems of Second Order Arithmetic by Stephen G. Simpson. The project of computable foundations of mathematics, for various definitions of the word computable, is a wide-ranging one, too large to include everything of relevance here. Keywords that might be helpful here include “constructivism”, eg Bishops Foundations of Constructive Analysis, “recursive analysis” and “recursive counterexamples”, and dependent type theory as is used in the programming languages Idris and LEAN.

To your second question, yes, the relation between statements that are independent of a set of axioms and numbers that cannot be computed is strong both intuitively and formally. The classic example of a statement that is independent of, say, ZFC, is that ZFC is consistent, which we’ll denote as $Con(ZFC)$. But $Con(ZFC)$ is equivalent to a statement about a particular computer program: “the computer program which searches over all the proofs in ZFC and halts upon finding a contradiction does not halt”. That in turn, is related to (among other uncomputable functions), the busy beaver function. In particular, suppose “the computer program which searches over all the proofs in ZFC and halts upon finding a contradiction” is a Turing machine with $X$ states. Then any proposition about the value of $\Sigma(X)$ implies either $Con(ZFC)$ or $\neg Con(ZFC)$, but as we know ZFC proves neither of those propositions, ZFC cannot prove $\Sigma(X)$ is equal to some specific finite value.

There is a subtlety here, as is partially addressed by r.e.s.’s answer: ZFC does prove the superficially-related statement “there exists some Turing machine which outputs $\Sigma(X)$”. But this is in some sense trivial, because ZFC proves the statements “there exists a Turing machine which outputs 1” and “there exists a Turing machine which outputs 2” and so forth, which lets it prove “for all natural numbers $n$, there exists a turning machine which outputs n”. Combined with the also-trivial statement “$\Sigma(X)$ is a natural number”, we of course now obtain “there exists some Turing machine which outputs $\Sigma(X)$”, but this sentence can now be seen to be not capturing what it might seem to mean. We don’t just want to know one of the Turing machines in the world outputs the number we’re looking for, we want to know which one, and there ZFC cannot help us. Indeed, any axiom system which is recursively enumerable (there exists a computer program which will print all of the possibly-infinite set of axioms) will eventually not prove $\Sigma(Y)$ for a sufficiently large Y, by the same argument given above.

For Adam Yedidia and Scott Aaronson’s proof that the value for Y in ZFC is at most 8000 (later reduced to 748), see A Relatively Small Turing Machine Whose Behavior Is Independentof Set Theory and Aaronson's blog post about it. For more on the busy beaver function and how it relates to the foundations of mathematics see Aaronson's The Busy Beaver Frontier.

I left your first question last because it is in some sense the thorniest and most philosophical. For example, it’s certainly true that ZFC (and indeed PA, and other quite weak systems of mathematics) prove the statement $$\Sigma(10^{100}, 10^{100}) \in \mathbb{N}$$ But I get the sense that’s not really what you’re asking. There is something philosophically uncomfortable about a number being proven to exist, but not being proven to have any specific value, which is one instance of the broader phenomenon of “non-constructive proofs”.

Different people have different reactions to this philosophical point. For example, the entire field of constructive mathematics is largely predicated on “we shouldn’t have numbers and more generally mathematical objects that are proven to exist, but not actually constructed”, for different formalizations of what exactly “constructed” means. Most mathematicians, on the other hand, either haven’t thought about this, don’t worry about this too much, or accept that they are working with objects that are (sometimes) fundamentally different from the ones which are computable. Two reasons to think that last idea isn’t too crazy: first, mathematics is always about figuring out unknown things. If I defined a number $Q$ via $Q = 1$ if $P \not= NP$ else $Q = 0$, then we also don’t have any good way to prove what the value of $Q$ is, even though most mathematicians think that ZFC proves that $Q=1$, and certainly that the value of $Q$ is not independent of ZFC. Second, this is more fuzzy, but a lot of mathematics relies on objects which at least intuitively aren’t computable, eg real numbers. The idea of an continuum of real numbers, which extends infinitely far in both directions and has no “gaps” is in some sense a very intuitive one, and doesn’t really accord very well with my picture of what things a computer can actually handle! You can encode real numbers as Cauchy sequences, (some of) which are representable as finite computer programs, but I certainly am not thinking most of the time about some computer program shuffling around (finite representations of) Cauchy sequences when I think about theorems like “every monotonically increasing sequence of real numbers has a least upper bound”.

Finally, though this answer has already grown very long, it probably wouldn’t be complete without at least a bit of a mention of one more philosophical point: formalism versus platonism. Briefly, formalism says “everything a mathematician does is encoded in the symbols, math is all about the formal derivation of theorems from axioms via proofs”, while platonism says “"mathematical objects really exist in some sense, there is some 'true actual' thing you mean when you say 'natural number', beyond the fact that your proofs about natural numbers correspond to symbols on a page which follow the mathematical rules of proof". This philosophical divide relates to our discussion above because (as far as I can tell) a formalist would say that there isn’t really a ‘fact of the matter’ about the value of $\Sigma(1000)$, or any other value of $\Sigma$ for that matter. There’s only the fact that ZFC proves $\Sigma(3)=6$, and ZFC doesn’t prove any value for $\Sigma(1000)$. While a platonist would say $\Sigma(3)$ really is 6, when I define a “natural number” and a computer programs and so on there is a real thing that I mean by that, they aren’t just symbols. Similarly, there is some true value of $\Sigma(1000)$, if you give me some particular computer program, if I ran it on my laptop it just would halt or wouldn’t halt, ZFC can’t prove that for all the programs, sure, but that doesn’t mean it isn’t true or false.

One reason to think this latter position makes sense is that there is only one axiom of the form $\Sigma(X)=n$, where $n$ is a decimal expansion of a natural number, that is consistent with ZFC (assuming ZFC is consistent). This is compatible with the fact that the value of $\Sigma(1000)$ is independent of ZFC because that simply guarantees (via Godel’s completeness theorem) there are two axioms that are both consistent with ZFC: $\Sigma(1000)=n$ and $\Sigma(1000) \not = n$, for some explicitly written out natural number $n$. Good luck figuring out what the relevant $n$ is though!

Is there some version of mathematics or system of axioms which resolves this problem? (i.e. where well-definedness of an object is equivalent to computability?)

There is a philosophy of mathematics known as constructivism which asserts that mathematical objects only exist if they can be constructed explicitly. "Well-defined" isn't really the right term here, we should stick with "exists", but in principle this should be the answer you're looking for. Quoth Wikipedia:

If, for instance, the algorithmic view is taken, then the reals as constructed here are essentially what classically would be called the computable numbers.