This throws some new light on why this MO question was hard to answer: mathoverflow.net/questions/93330/…

@Andres: I was in Göttingen in 2002 (so my memory is fading a bit) and I was shown the book of Hermes' calculations by the number theorist S. J. Patterson. It is a very meticulous hand written book, but Patterson's opinion was that Hermes does not reach a clear solution of the equation. I wrote a little more about this, see tech.groups.yahoo.com/group/Hyacinthos/message/10294

But Hardy goes on to say "I have heard Professor Eddington, for example, maintain that proof, as pure mathematicians understand it, is really quite uninteresting and unimportant, and that no one who is really certain that he has found something good should waste his time looking for proof.... [This opinion], with which I am sure that almost all physicists agree at the bottom of their hearts, is one to which a mathematician ought to have some reply."

@Ali. Thanks, that's interesting. I guess that Sack's result was quickly superseded by Solovay's; but still, the Sacks paper came out first.

@Joel. It may well be that "measure-theoretic uniformity" got subsumed by "random real forcing," but if so I'm still puzzled by the lack of citations of Sacks' paper. Also by the lack of emphasis that "ZF + DC + all sets of reals are measurable" holds with probability 1. You're right that Sacks' proof must assume the existence of an inaccessible; I'm not sure exactly what role it plays.

+1 for the nuanced interpretation of "used."

Thanks, Alexandre. This shows that the opinion has been around longer than I first thought.

@Daniel Groves. Sorry, I should have read further into your paper.

@Andy Putman. By the reduction of special c.e. sets to a universal set, there is a computable function $f$ such that a group presentation $p$ will be of a 3-manifold group if and only if $f(p)$ is a word equal to 1 in a suitable finitely presented group $G$. For this "one-one reducibility" of arbitrary c.e. sets to a universal set, see e.g. Hartley Rogers Theory of Recursive Functions and Effective Computability, pp. 80--82. Getting a universal $G$ is hard, but fairly immediate from the usual proofs that the word problem is unsolvable, I think.

Regarding the main theorem of GMW, that recognizing presentations of 3-manifold groups is reducible to the word problem; doesn't this follow from general theorems about c.e. sets? The word problem is equivalent to the membership problem for a universal c.e. set. Deciding whether a presentation is of a 3-manifold group is equivalent to the membership problem for a particular c.e. set, because one can list all 3-manifolds (say, as simplicial complexes) and hence the presentations of their groups. Hence the latter problem is reducible to the word problem, or am I missing something?