What is the intuitionist / contructivist view of the Fermat theorem proof?

Question

Since Wiles proof is in essence proof by contradiction, it relies on the law of excluded middle. Which as I understand intuitionists / constructivists do not accept as an axiom. So what is their view of the Wiles proof? Do they still consider Fermat theorem not proved?

Answer 1

Wiles' proof is not, in essence, a proof by contradiction.

Wiles has shown that every elliptic curve over $\mathbb{Q}$ (well, a large enough subset of them) satisfies the following theorem. At the time, this was a conjecture, and a big one, and Wiles had begun his work on FLT after a connection was established between FLT and this conjecture.

A positive integer solution to FLT could be manipulated to construct an elliptic curve which isn't modular, but this kind of connection is only an indication that the modularity conjecture would imply FLT. So FLT would not be proven by assuming it's true and seeing it's impossible, but rather it was already established that if FLT is true, then something really strange happens, and Wiles had undertaken to prove that it was impossible.

Wiles, in fact, uses the word contradiction only 3 times throughout his amazing paper "Modular elliptic curves and Fermat's last theorem.". FLT isn't even stated directly after modularity is proven, since the connection was already known,

As for the proof itself, it was accepted as correct (not without some obstacles), and still is accepted, and will remain so. Wiles was awarded, among many other honors, a special plaque from the ICM (I heard someone refer to it as a "quantized" Fields medal), and in 2016 he was awarded the Abel prize.

Answer 2

There is a very subtle difference between proof of negation and proof by contradiction in constructive mathematics. If you assume some $A$ and derive a contradiction then you conclude $\lnot A$. In fact, this is how we define negation. Now on the other hand a proof by contradiction assumes for some $A$ that $\lnot A$ holds and derives a contradiction. By the definition of negation they have shown $\lnot \lnot A$ but with the double negation law (equivalent to Excluded middle) they can then conclude $A$.

The wiles proof assumes that there is a solution and shows a contradiction. This is proof of negation. So we may conclude $\lnot (\exists x, \phi(x))$. Where $\phi$ is some encoding of fermats last theorem. Now it is constructively valid to then conclude $\forall x, \lnot \phi(x)$. I’ll try to link a good reference that discusses the demorgan identities that do hold constructively (not all of them do.)