FOM: Dirichlet and Wiles

[JSHIPMAN@bloomberg.net]

I will have to try to find the Zassenhaus paper; apparently I was misinformed
about the existence of an elementary proof of Dirichlet's theorem.  (I wish
I could remember where I'd read that none had been found.)  The reason that
would have been a good test case is the theorem has been around for 150 years
and is presumably very well-understood by now.  Of course Wiles's theorem is
even easier to state than Dirichlet's but there is obviously no hope of an
elementary proof in the near future.  Questions for FOM:
    1) "How much" in the way of axioms did Wiles use?  What is the simplest
system his proof can be formalized in?  Is it easy to put it in full
second-order arithmetic?
    2) If an elementary proof were discovered, would this be a big deal?  Why?
    3) What would we make of a result that a "nonelementary" proof can be
converted to an elementary one where the resulting "elementary" proof is too big
to "fit in the margin" (read: to be humanly readable)?  Steve, do your
conservative extension results give blowups in length of proofs? -- Joe Shipman