As François points out in his MO comment on the deleted question, and as noted by Andy above, the same question was asked on MSE - math.stackexchange.com/questions/618147.

Currently the question is closed there (as a duplicate [correction: now as "too broad" after a second closure, as mentioned by Asaf in a comment below]; indeed there was another question which brought up the issue of FLT and AC, and it was given an answer very similar to the response of Andres indicated below). If anyone is interested in this, they probably should have a look at the MSE discussion. There is also a lengthy MSE *meta* discussion attached to it.

Of course you (Makoto) are welcome to open a discussion about the suitability of this question for MO. If other MO users would like to see this question opened here, then by all means they should weigh in with an answer or comment. But I would like summarize some of the relevant MSE comments (and one of the comments at MO, which some can't see):

The question received substantial and authoritative response, notably by Andres Caicedo. Paraphrasing what he wrote (I ask the experts to correct me if I garble this in any way), for any universe $V$ that models ZF, FLT holds in $V$ iff it holds in the subuniverse of constructible sets $L$, because the statement of FLT is an arithmetic statement. But FLT is provable in ZFC (NB: without assuming an inaccessible cardinal according to all the experts; see the last discussion that Makoto links to). Therefore it holds in any model of ZFC, such as $L$, and hence it holds in $V$ as already mentioned. Since it holds in every model $V$ of ZF, it is provable in ZF by Gödel's completeness theorem. (This may be even too heavy-handed an explanation, but it's what I came up with.)

Makoto edited his question to say he was not particularly interested in whether FLT could be proven without AC, but whether AC could be removed from *Wiles's proof*. I don't know what this could mean if Andres's response (which I thought was excellent) is deemed inadequate by Makoto. At some point Makoto wrote at MSE meta: "That a proof exists does not necessarily mean a human being can ever actually come up with it. Anyway, I'm asking whether AC can be removed from the Wiles's proof. Nobody has answered it yet." Andres responded to that a little later, and couldn't have been clearer: *any* proof of an *arithmetic statement* [my emphasis] like FLT, including Wiles's (which without doubt passes *inter alia* through some heavy machinery, going into the proof of his Modularity Theorem), can be formalized in ZF, and the mechanism for doing that is well-understood by set-theorists.

In what I thought was a real clincher for this line of argument, MO user Yury cleverly summed things up in his MO comment: "As @FernandoMuro points out, it is extremely unlikely that the proof can be formalized in ZF without any changes. However, one can add just one sentence in the beginning of the proof to make it a proof formalizable in ZF: “all the formulas below are relativized to L (the constructible universe)”." It would be hilarious if Wiles had actually written a paper on FLT with that declaration appearing in section 1! His audience would think he'd gone mental. But note that such a meta-declaration would be in force all throughout the complicated argument, the Modularity Theorem, the whole schmeer in fact, and then just before the final QED which ends the proof of FLT, he brings in the remarks about arithmeticity and Shoenfield Absoluteness or whatnot. So his proof would be a few lines longer.

I think what I personally take away from that is that Andres (and Yury at MO, but this is not visible to users with < 10k rep) gave a very satisfactory mathematical response to *the question as asked*, as did André Nicolas in a very similar answer to the MSE question cited as duplicate. If Makoto (or anyone else for that matter) wants to ask a separate question about the use of AC in the proof of a (possibly) *non-arithmetical* statement, such as what might possibly appear as some lemma buried somewhere in Wiles's opus, then that would be *an entirely different question*. [It would not be reasonable to request that someone scour several hundred pages of Wiles's material just to ferret out such a sublemma -- that's the questioner's duty, and it's the issue underlying the "too broad" reason for the second closure.]

And now a true "meta" comment, since much of the above has technical mathematical content which is arguably not the real concern of MO meta (but which may have been necessary to fully establish the context). The decision of François to delete the question from MO was made no doubt in part because it's been answered already. But *possibly* also for the very pragmatic reason that, based on prior experience, many users will be completely put out by the prospect of seeing another discussion dragged out, arguing over the meaning of a question in a whole bunch of comment boxes, just as it currently played out at MSE. Personally, I think one gracious thing to do would have been to *thank* Andres for his terrific answer (please note he was one very cool cat throughout the entire discussion: utterly calm and professional in fact).

I don't understand why you (Makoto) don't do that more often: thank your respondents for their insights and seek to resolve issues with grace and dispatch.
It is regrettable, but I'm afraid many here feel it is a waste of time trying to engage with you, because of patterns as well exemplified in the MSE thread and elsewhere, where discussions go on and on and are never resolved to your satisfaction. This is frustrating for people who are busy as it is. Changing people's perceptions about that will be hard, I'm afraid.

Why on earth did you think it would be acceptable here?There are two reasons. One is that MSE and MO are different sites. The other is that a similar question as mine was accepted in MO. $\endgroup$ – Makoto Kato Jan 1 '14 at 1:19subjectivematter whether a question is closed or not. Hence a fact that a question was closed in MSE does not necessarily means that it should be closed in MO. $\endgroup$ – Makoto Kato Jan 1 '14 at 1:40did you really think people wouldn't notice?] Of course, not. I knew sombody like you who were watching my posts in MSE would find it out right away. $\endgroup$ – Makoto Kato Jan 1 '14 at 19:04You're just unaware.] What's your definition of meta spamming? $\endgroup$ – Makoto Kato Jan 5 '14 at 18:55