User richard elwes - MathOverflow

Answer by Richard Elwes for Not especially famous, long-open problems which anyone can understand

2012-07-24T13:05:57Z

How many trees are there?

Let $T(n)$ be the number of trees on $n$ vertices up to graph isomorphism. There is no known closed formula for $T(n)$.

In 1947 Richard Otter proved^[Source] the asymptotic result $$T(n) \sim A \cdot B^n \cdot n^{-\frac{5}{2}}$$ where $A \approx 0.535$ & $B \approx 2.996$.

By way of contrast, let $L(n)$ be the number of labelled trees, i.e. trees formed from vertices labelled $1,...,n$ where isomorphism additionally preseves the label. In 1889, Arthur Cayley showed^[Source] that $$L(n)=n^{n-2}$$

Answer by Richard Elwes for Inaccessible cardinals and Andrew Wiles's proof

2010-08-16T20:55:26Z

Can I draw attention to the continuation of that quotation? "But there is a general consensus among mathematicians that this was just a convenient short cut rather than a logical necessity. With a little work, Wiles's proof should be translatable into Peano arithmetic or some slight extension of it."

For the record, McLarty's paper in the Bulletin of Symbolic Logic was indeed the source for my claim that Wiles used an inaccessible cardinal (via Universes). If anyone fancies debating the exact definition of 'using' an axiom without 'needing' it, and whether or not that definition applies in the current case, we should probably do it somewhere else (Pedantry Overflow?). But I explicitly opposed the claim that the proof 'needed' large cardinal assumptions, so I don't propose to be too apologetic.

Anyway, it's an interesting question, and I'd be pleased if my article goes some way to bringing an answer into the public domain (even if I do get my head shot off in the process ;) ).

(Incidentally I would rather have left this as a comment than an answer, but don't have enough (any) reputation points. If anyone with superpowers wants to move it, please go ahead.)

Comment by Richard Elwes

2011-03-21T12:03:02Z

I heard Angus Macintyre talk about it fairly recently. The situation is a little unusual, as to write out a proof fully would entail multiplying the (already considerable) length of Wiles' proof by 5 (or 10 or something), to reduce every single step to PA. Macintyre does not intend to do this in full completeness, but he is continuing to prepare a manuscript to show that the key pieces of higher order machinery used in the Wiles' proof can be translated into PA. The focus is on the central modularity theorem, which he will show is effectively $\Pi^0_1$, and provable in PA.

Comment by Richard Elwes

2010-08-17T07:05:05Z

Ok! Try again... Macintyre has reportedly announced a proof (which I would expect to be non-trivial) that Wiles' proof can be translated into PA. In the intro to his forthcoming book, Boolean Relation Theory and Incompleteneess, Harvey Friedman conjectures that it should be proveable in an elementary fragment $I \Sigma_0(exp)$. This is an instance of his conjecture that "Every theorem published in the Annals of Mathematics whose statement involves only finitary mathematical objects (i.e., what logicians call an arithmetical statement) can be proved in elementary arithmetic."

Comment by Richard Elwes

2010-08-16T23:30:03Z

I now seem to have magically acquired enough reputation to comment... Very recently I have read that Angus Macintyre has announced a proof of FLT in PA. The only reference I can provide is this: cameroncounts.wordpress.com/2010/01/07/…