Can computers write proofs

that human being can understand? By that I mean not those formal logic nonsense. Tim Gowers is doing an interesting experiment to get readers to judge proofs of exercises in metric space theory. The three proofs are supposed to be written by an undergraduate, a phd student and a computer. I only looked at the first problem which is quite straightforward: prove that the intersection of two open metric spaces is open.

Honestly, I can’t tell which one is the computer. The main problem is one does not know how the program was written. Here’s my analysis of the solutions. The first two proofs are very similar in the sense that they both use open balls. (The third did not.) The writing is also much clearer with good choice of notations. One thing that is clear is that the first two writers already knew what is the key to the proof – take the minimum of the the radii of the two open balls. The third proof, on the other hand, seemed to be using the various conditions to force the choice. Perhaps that makes it the computer, assuming that the programmer do not actually instruct the computer to reorganize and rewrite the proof. If the first two were humans, I still cannot tell which is which. The second proof looks to be more carefully written, but that does not actually imply the level of mathematical sophistication. Or does it?

This entry was posted in Geometry/Topology, Problems, Technology. Bookmark the permalink.

Leave a Reply

Your email address will not be published.

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>