Which write-up for Problem 1 did the computer write? (Poll Closed)

1,260 Total Votes

  • ricardo - 7 years ago

    In (c) the "author" worked backwards to conclude that min(r,r') was the correct radius. Even if a person had to think a little to reach that conclusion they would still prefer to write the argument in the direct order.
    For me using distances instead of balls was not a tell a person could still think in terms of distances for sport or some other reason.

  • Stephen P. Schaefer - 7 years ago

    I barely remembered the definition of "open", and wondered where this term "ball" came from. After reading all three proofs, I was more certain of my memory, and actually found the third more precise and less confusing through its avoidance of inessential entities. I'm guessing this "ball" is how they teach open sets in "metrics" - I'm (barely) a programmer, and I only appreciate mathematics, so maybe that's why I found 1c both more convincing and more machine like.

  • Freek - 7 years ago

    In all cases there is exactly one option that ends with "we are done"?

  • Michael Kolczynski - 7 years ago

    C) is computer generated because it is written as close to the logical path as possible. Each other uses human expressions. Sure, you could have all sorts of systems built to convert the system's logic into more human like expressions, but I would assume the only goal is to have the deduce proofs, therefore an efficient human would code a verbose mode for the logical path. It's easiest to see a => b as being written, "therefore, since a, b"

    Using the term Ball in a proof requires auxiliary knowledge about what a Ball is, whereas C) just needs to understand a little about the function d(,).

    I would be really interested in seeing the system find a contradiction. This seems like a path-finding algorithm based on truth evaluations.

  • Giuseppe Ottaviano - 7 years ago

    If my guess is correct and (c) is the computer-generated version, the fact that the proofs always end with "and we are done" give it away. In fact, the proofs that end like that look somewhat lower-level and redundant.

  • Murray Lark - 7 years ago

    1 c probably because the ball notation allows greater concision

  • Theresia Eisenkoelbl - 7 years ago

    Your poll lacks the option: I hope that answer (x) was not written by a human. Incidentally, reading the answer 1 (c) in the preceding post made me decide not to answer the previous poll.

  • Sameer R Kulkarni - 7 years ago

    Both (a) and (b) worked out in terms of balls but (c) uses the distance directly. And also so much analysis has been done to find that the required radius is min(r,r'). A computer can only do things by brute force, so thought (c) was by computer. I have very limited knowledge of programming hence I'm not certain.

Leave a Comment

0/4000 chars

Submit Comment

Create your own.

Opinions! We all have them. Find out what people really think with polls and surveys from Crowdsignal.