Gustavo Lacerda

This note by John McCarthy from 1964 is about a sort of obfuscated-proof-contest.

This Stanford AI Memo of 1964 illustrated the fact that a theorem may not be easy to prove if the proof involves an idea not expressible in the language in which the theorem is stated.

Here's an exercise for the readers of this blog:

Prove that all Manhattan polygons (i.e. all lines are either horizontal or vertical) have an even number of corners. (credits to someone I'll leave anonymous just in case)

How many distinct proofs can you come up with? (What counts as distinct proofs is an interesting question to formalize (proof identity))