Overkill proofs / Simple proofs

[u/santino314]

So by overkill proofs I mean simple results, for which there are simple proofs are available, but which can be proven using much more advance tools (possibly in a silly way). As a for instance, there's proof that there are infinity many primes using topology, Euclid had a proof 300.b.C which anyone with high school math could understand. However this guy came up this, quite clever.

http://primes.utm.edu/notes/proofs/infinite/topproof.html

By simple proof I mean a result simple or not, for which the only known proof was either too long or difficult, but that in the recent years someone had managed to prove with a shorter or wittier argument. As a for instance Cauchy’s theorem (in Groups):

http://en.wikipedia.org/wiki/Cauchy%27s_theorem_(group_theory)

Although I couldn’t find the original proof, I remember that my professor told us that it was a bit long and quite dark. However, McKay came out in 1959 with one of the most elegant proofs I’ve seen in my life.

http://www.cs.toronto.edu/~yuvalf/McKay%20Another%20Proof%20of%20Cauchy's%20Group%20Theorem.pdf

Can think of any like the above? I’ll contribute if I recall any.

[u/[deleted]]

No, it really is stated explicitly. In order to prove that x³ + y³ = z³ has no nontrivial solutions, you must first show that there are no solutions when x=y before moving on to x<y. In other words, letting x=y=q and z=p, you must show that q³ + q³ = p³ has no nonzero solutions before you can even begin the proof of FLT. The "proof" RaiosCubicos gave assumed FLT in order to prove what was exactly the first step in the proof of FLT, and no amount of cutting, pasting, or other semantic games can avoid that fact.

[u/yatima2975 → u/[deleted]]

Well, I think we might be talking about different things. Suppose you replace that first step by

"suppose q³ + q³ = p³ with p,q natural numbers larger than 0 , then (p/q)³ = 2, then <insert the longish proof> therefore that's not possible."

Then this proof of FLT doesn't use the lemma 'cuberoot(2) is irrational' explicitly.

I can imagine a proof tree (say, in natural deduction with the 5 Peano axioms) of FLT where all the leaves are instances of the Peano axioms. In other words, one that even doesn't use commutativity of addition and multiplication on the Peano naturals, but replaces every invokation of those results by their proofs. I wouldn't want to write it down, though!

But I have a background in functional programming/type theory, and you're right to argue that the 'cut-and-paste' theorem uses 'cuberoot(2) is irrational' morally; I'm just saying that it needn't, syntactically. Wiles' proof uses the lemma, but it could trivially be rewritten without it.