@Todd, you may want to add a comment here (not under this answer, but rather under Joël's original post, for the sake of visibility) indicating that the question is now locked, and perhaps mentioning what led you to do this.

"What would the evidence be?" There is the biography by Scharlau, see here, based on extensive interviews. Anyway, the (finally closed) question is redundant, and asked in a very unprofessional manner.

If you ask the question that way, I would vote to close. It feels like a fishing expedition and not a real question. Are there reasons why you suspect there is such a connection? You should mention these reasons as explicitly as possible. Even better if you know of any literature where cellular automata have been applied to related concepts, something concrete that would indicate that there is some hope for this to be the case.

Jack, the proposal has just reached the commitment phase! You may want to write a follow-up post.

"Those people"?

Add the real-analysis tag, but leave the others as well.

@Emerton Thanks for the comments, and I agree with the goal you describe. That is why I find McLarty's program and similar others worthwhile, since the outcome should be our true understanding of the arguments behind the proof. (I mention McLarty's since it has been mentioned before, but I do not think this is the only path to a purely number-theoretic proof; in fact, I sometimes feel that the emphasis by some on first order $\mathsf{PA}$ ends up being a bit of a distraction here.)

My point in mentioning this is that I have seen the criticism that the translation-to-$L$ argument gives us "non-canonical" constructions, while the opposite is in fact true. One can think of the whole thing as showing that we have explicit, canonical choice functions in the case under consideration, so we are not actually making any appeals to the axiom of choice, since choice is provable in the relevant instances. (On the other hand, the proof is definitely non-finitary.)

Let me add, Todd, that the mention of the completeness theorem is somewhat distracting, as it makes it appear as if Shoenfield's absoluteness is a metamahematical trick. Though it needs some understanding of set theory, the argument is much closer to classical analysis. In fact, what one does is to associate to each $\Sigma^1_2$ set a tree representation. Shoenfield's absoluteness is simply the fact that a $\Sigma^1_2$ statement holds iff the associated tree is illfounded. (Cont.)

The modularity theorem is $\Sigma^1_2$ (this is an overkill), so Shoenfield absoluteness applies to it as well.

I agree. And yes, having the proof-theory tag is definitely a red flag; removing it from the question would already be an improvement.

Ah, that may be it.

(I may misremember. Probably buried somewhere on tea. I'll post a link if I manage to find it...)