A second experiment concerning mathematical writing
gowers.wordpress.com
gowers.wordpress.com
Because it spells things out like a careful someone just learning (uses "so" less, the mature person is also apart) it would be a good tool for exposition. By that token I can also guess the grad student as the one who seems most comfortable (and also for favoring "take" and for all style statements while using "exist" and "since" least). This is most interesting for what it says about teaching and how internalized understanding makes teaching hard: expertise is an iceberg floating in a sea of unconscious reasoning. My guesses:
========
grad student: b, c,a, b,a
bot: c, a, b,c,c
It randomly generates math papers, one of which was [accepted by a peer-reviewed journal](http://science.slashdot.org/story/12/10/19/1256216/randomly-...)
Then (b) could be the PhD student who talked to enough people to be aware that you never know what others consider a ball.
Finally, (c) goes to computer because it's the longest one and it's full of Greek letters. I've known a PhD who believed only in proofs starting with "For arbitrary ε > 0, take δ = ...", but even he wasn't as boring as (c).
There's a line in that proof saying r=min{a,b}; normally I take that to mean r is the minimum of a and b (which makes the proof wrong, since not all metric spaces have obvious orderings on their elements. Spaces like the complex plane or the 2d plane, with an appropriate metric, for instance.
I suppose it could mean r is the point in {a,b} such that the ball B_a(x) or B_b(x) has the smallest radius - but that looks more like a human making a notational mistake, particularly given that both 1b) and 1c) use min(,) in a way that seems correct to me (since they're using min on the values of the metric, not the elements of the metric space.
AFAICT, either the prover made a mistake in logic or a mistake with notation - which I reckon makes him or her human.
Then again, it's been years and years since I thought about this stuff, and I was prone to making mistakes all the time when I did, so everything above might well be wrong. My neurons are getting all fuzzy these days.
I agree with you though, I don't think it's option (a)
Your reasoning here is wrong. The "a" and "b" come from the range space of the metric, which by definition associates a pair of points in the metric space (unnamed, but call it X) with a nonnegative real number.
In short, "a" and "b" are in R, not in the original metric space X, so it's legal to take the lesser of a and b.
Even though I chose (a), and like my argument, I find some of the arguments here for (c) convincing as well.
I could not proceed farther than question 1, because I'm kind of tired of real analysis at this point. Certainly not on Sunday morning. ;-)
One of my theories so far is those computer-generated proofs don't use triple equalities (e.g. "a = b = c") even though it makes a better explanation in certain limited situations.