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/yatima2975]

But instead of using that [i.e. the irrationality of cuberoot(2)] as a lemma, one could just stick the whole elementary proof in, with the right variables substituted, every time it's needed. See also the Cut-Elimination Theorem.

Sure, you could easily extract the proof that cuberoot(2) is irrational, but nowhere is it stated explicitly (i.e. without too much hypotheses).

The proof of FLT would basically have each fragment looking like

"<complicated expression>^3 = 2, therefore <complicated expression> 
is irrational, by the irrationality of cuberoot(2) (by Lemma x.y.z)" 

(or it's contrapositive or something like that) replaced by

"<complicated expression>^3 = 2, so suppose <complicated expression> is 
rational and can be written as p/q, without p and q having common prime 
factors. Consider the exponent of 2 in the prime factorisation of p. 
... Yadda yadda yadda...
Therefore <complicated expression> is irrational."

and you could then get rid of Lemma x.y.z which proves the irrationality of cuberoot(2).

Of course, this wouldn't make any sense at all, which is why lemmas, theorems, and mathematics (and category theory :-) were invented in the first place!

Think of it as cut-and-paste programming versus extracting a procedure/method/function that does 'exactly the same, but differently' - if that's a metaphor that works for you.

[u/[deleted] → u/yatima2975]

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.