> >I've been told that Wiles' proof rests on a result that was proven using the >consequence of the axiom of choice that a certain extension of the p-adics >which is both algebraically closed and complete in the p-adic metric is >isomorphic as a field to (a subset of?) the complex numbers. Now, we know >that any proof of Fermat's Last Theorem (or even of the modularity conjecture) >which uses the axiom of choice doesn't really need it. But I don't know whether >there's any non-messy automatic way of extracting it from the proof. > >Keith Ramsay > > > Shouldn't Wiles proof goes through in second-order PA ?
If it doesn't, then I'm afraid here's one vote for saying he hasn't really proved FLT, and JH still has a chance.
