Stop here if you haven't taken the poll. I think it is very readable but gives itself away by favoring certain phrases which suggest a template. Phrases like "we are done", "whenever", "therefore,[setting]". All the proofs are terse in general but it tends to spell things out more carefully than humans who prefer to string ideas using conjunctions and leave obvious basics as implicit.
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:
Great observation. I didn't make it past the first problem, but I chose (c) as well. Reason being, that proof seems to have the least, shall we say, semantic depth (I'm just making up terms here). It invokes the least amount of meaning / refers to the fewest concepts per statement. Interestingly, not only is this a sign of having been produced automatically, it can often be a positive thing in terms of mathematical style.
I'm not sure of any of my answers, but I guessed the computer generated proofs are: 1c, 2a, 3b, 4c, and 5c. These proofs seem to be the most uniform in language, especially the way they all end with "we are done". I was the least certain about 4c since this option doesn't seem in the established style of the computer (assuming my other guesses were correct).
From the post: "I would also be interested in comments about how you came to your judgments. All comments on both experiments and all votes in the polls will be kept private until I decide that it is time to finish the second experiment."
A lot of people read Gower's blog as it has some really useful expositions of undergraduate maths, which he makes available for anybody who might find them useful. In that sense I think he is justified in not providing a reward; you don't have to do the test if you don't want to anyway. He will no doubt post later with the actual writers' identities.
I think (a) may be the undergrad student - still young and idealistic :)
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).
I chose (a) also, not because of the restatement, but because it proceeded in such an orderly way, without doubling back. E.g., halfway through (c), there's a sentence starting "We would like to find...", which interrupts the deductive steps to insert an end-goal. It seems unnatural.
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. ;-)
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.
"...which makes the proof wrong, since not all metric spaces have obvious orderings on their elements..."
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.
a and b are real numbers, namely the radius of two balls. They forgot to define B_a, but typically
B_a(x) := {y in X : d(x, y) < a}
where (X,d) is the metric space.
I agree with you though, I don't think it's option (a)
It's almost certainly (c), and the rest of the ones that end with "and we're done". The first one is probably not (a) because it has a pronoun ("it's"), which would be a pain to program into a natural language process for this limited purpose.
I answered three of those where I didn't have to think too hard to follow the reasoning. It would be nice to have the answers eventually after the experiment is over.
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.
I only answered the first one, but it was my impression that 1c was generated by the computer as it used weird greek letters; I have never seen eta used in that setting before, and I doubt that a grad student or an undergrad would be inclined to break convention.
not too long ago I attended a talk by Thomas Hales (proved the Honeycomb conjecture and the Kepler conjecture) where he talked in detail about his Flyspeck project, which he says has just a 400 line kernel that traces every line of a proof down to the axioms, that will formalize his proof of the Kepler conjecture and many questions in the Q&A after had to do with curiosity of machines being able to do exactly this. very interesting
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