Or, maybe he had a sense of humor, and made his margin annotation knowing full well that this would cause a lot of headscratching. It may well be the first recorded version of nerdsniping.

What are some believable but wrong proofs of FLT? Wikipedia also claims that there were historically a lot of them[1], but doesn't provide examples.

[1]: https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem#Prizes...

It was called Fermat's last theorem because it was the only one of the theorems stated by Fermat that remained to be proved at the time

Yeah, I just figured out how to simply reconcile general relativity and quantum mechanics, but I am writing on my phone and it's too tedius to write here.

    import FLT 
    theorem PNat.pow_add_pow_ne_pow
        (x y z : ℕ+)
        (n : ℕ) (hn : n > 2) :
        x^n + y^n ≠ z^n := PNat.pow_add_pow_ne_pow_of_FermatLastTheorem FLT.Wiles_Taylor_Wiles x y z n hn

Unlikely, but not unheard of. Fermat's theorem on sums of two squares is from 1640. https://en.wikipedia.org/wiki/Fermat%27s_theorem_on_sums_of_... says:

“Fermat usually did not write down proofs of his claims, and he did not provide a proof of this statement. The first proof was found by Euler after much effort and is based on infinite descent. He announced it in two letters to Goldbach, on May 6, 1747 and on April 12, 1749; he published the detailed proof in two articles (between 1752 and 1755)

[…]

Zagier presented a non-constructive one-sentence proof in 1990“

(https://www.quora.com/What-s-the-closest-thing-to-magic-that... shows that proof was a bit dense, but experts in the field will be able to fill in the details in that proof)

Well, true, we cannot be 100% certain, but if he published the proof to n=4, we can say it's most likely he did not find the general proof.

Even super simple results like uniqueness of prime factorisation can pages of foundational mathematics to formalise rigorously. The Principia Mathematica famously takes entire chapters to talk about natural numbers (although it's not ZFC, to be fair). For that reason I think it's pretty unlikely.

> we have an upper bound

Is Wiles' proof even in ZFC?

No, the consensus among mathematicians is that Fermat did not have a proof.

No support for symbols, amirite?

This is actually way false. Rigorous mathematical proof goes back to at least 300 BCE with Euclid's elements.

Fermat lived before the synthesis of calculus. People often talk about the period between the initial synthesis of calculus (around the time Fermat died) and the arrival of epsilon-delta proofs (around 200 years later) as being a kind of rigor gap in calculus.

But the infinitesimal methods used before epsilon-delta have been redeemed by the work on nonstandard analysis. And you occasionally hear other stories that can often be attributed to older mathematicians using a different definition of limit or integral etc than we typically use.

There were some periods and schools where rigor was taken more seriously than others, but the 1600s definitely do not predate the existence of mathematical rigor.

It is possible to discover mathematical relation haphazardly, in the style of a numerologist, just by noticing patterns, there are gradations of rigor.

One could argue, being a lawyer put Fermat in the more rigorous bracket of contemporary mathematicians at least.

Not true. Even if it’s more strict it’s just a matter of inserting more care and steps, not changing the original idea.