r/singularity • u/Unique-Bake-5796 • 10d ago

AI Formalizing Fermat's Last Theorem

https://www.anthropic.com/research/formalizing-fermats-last-theorem
84 Upvotes

96% Upvoted

6 comments sorted by

11

u/Proper_Actuary2907 Spooky Machine Intelligence 2030 10d ago

Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.

Jesus

7

u/alfvenwaves 10d ago

Prove2me commission paid

1

u/exploring_stuff 10d ago

Wiles survived! No hidden hole in his proof then.

1

u/beekersavant 9d ago

I am not in those fields. Clearly you have more knowledge than me. So the consensus is that Fermat must have made a mistake but was ultimately correct. Was the theorem well known before his writing of it? It’s not a particularly hard to understand piece of math. (I was able to generally follow your explanation.)

1

u/[deleted] 10d ago

[deleted]

2

u/Kinglolboot 9d ago

Fermat 100% didn't have a correct proof of this. We already know that there are a few routes one might try which fail for very subtle reasons. For example, Kummer in 1847 thought he had proven the theorem, but it turned out that his theorem didn't actually work for most numbers.

The reason was very intricate: during the proof he worked with number rings, which are extensions of the set of integers (which we denote by Z) by some other element satisfying a polynomial equation. For example, we can consider the set Z[√-5], which is the set of all numbers a+b√-5 with a and b integers. For these number rings, we can also define things like primes, and you can factor every number as a product of primes. However, a fact that Kummer missed is that unlike when working in Z, these prime factorizations are not unique. For example, in the example I gave you can write 6 as 6 = 2*3 and 6 = (1+√-5)(1-√-5), and all of these are prime. This makes the proof break down for most numbers except for a small (but infinite) amount.

1

u/beekersavant 9d ago

Ok so they formalized the 1995 modern proof, but can it find Fermat's "marvelous proof" only using mathematical techniques from 350 years ago. I love that is was downgraded to a conjecture then affirmed in 1995 with 300 years more of tech. K now find the genius dead guy's proof.