HN Explorer

Ask HN: Will an AI be able to prove Fermat's last theorem? When?

2 points by logicallee ↗ HN
Do you think an AI will ever be able to correctly answer a prompt like: "Prove Fermat's last theorem in a rigorous way. Produce a proof that can be checked by Coq, Isabelle, Mizar, or HOL in a format supported directly by any of them" and have its output really work and prove it? If so when?

16 comments

[ 2.9 ms ] story [ 50.5 ms ] thread
bell-cot
Literally "ever"? Yes.

In a short-term-obsessed online world, where "forever" is just a few years? Probably no.

zephyrfalcon
Fermat's Last Theorem was proven by Andrew Wiles in 1994 after centuries of attempts. While artificial intelligence (AI) has made significant strides in mathematical research and theorem proving, the proof of Fermat's Last Theorem required a highly specialized understanding of mathematics, particularly in the field of number theory.

It's challenging to predict with certainty when AI might independently prove such a complex theorem. While AI systems can certainly assist mathematicians in exploring mathematical concepts and even discovering new theorems, the level of creativity, insight, and intuition required to solve problems like Fermat's Last Theorem is still largely within the domain of human mathematicians. However, AI may contribute indirectly by aiding in the exploration of vast mathematical spaces and providing tools for verification and validation of proofs.

eimrine
I don't think any capitalist would like to fund that service. In my opinion AI movement is going to migrate in easier fields then Math, such as k*ing people with a drone swarm. It can not grow into something more than one guy's farm of videocards.
levn11
https://www.techrxiv.org/users/717330/articles/702287-on-fer...
n4r9
On p.4 you argue that for integers a, b, c and n:

  (a + b − c)^n = (c − a)(c − b)g_1(n)

  => a + b − c = [(c − a)(c − b)g_1(n)]^(1/n)

  => g_1(n) | a + b - c
This doesn't follow as it stands. For example, if a=b=3 and c=n=2, then g_1(n)=16 whereas a + b - c = 4.
levn11
This is only true for a,b,c that satisfies a^2+b^2=c^2.

So a=b=3 and c=n=2 is not part of the solution set.

n4r9
But you're not using a^n+b^n=c^n in your argument at the bottom of p.4. You just say "therefore g_1(n) divides a+b-c". My example shows that yhe implication doesn't follow in general. And it's not clear why it follows specifically if a,b,c are a solution to FLT.
levn11
i believe you skipped pages 1-3. g_1(2)=2 for all a,b,c with n=2. g(n) carries with it the assumption of a^n+b^n=c^n as i showed in pages 1-3.
n4r9
Pages 1-3 simply show that (c-a) and (b-a) divide (a+b-c)^n (for even n), assuming they are a solution to FLT.

You then define g to be (a+b-c)^n/(c-a)(b-a), an integer.

I follow you this far. I do not see why g divides a+b-c, and I don't think the argument on p.4 proves it.

levn11
it's a proof by contradiction. g would divide a+b-c IF a+b-c are integers.

for n=2, g(2)=(c-a)(c-b)g_1(2) and g_1(2)=2.

So only when n=2 is it true that g divides a+b-c.

Otherwise we get a contradiction that it divides. since then, g_1(n) for n>2 is not a factor of a+b-c, we can safely assume at least one of them was not an integer.

n4r9
I honestly don't follow your last sentence. Why does g not being a factor of a+b-c mean they're not integers?
levn11
it follows specifically from the form on pages 1-3. i would recommend reading it with fresh eyes after a good night's rest.
n4r9
It doesn't follow from anything on p1-3. Certainly not directly. If you were being genuine about this I think you would appreciate an opportunity to improve the proof rather than resort to insults!
levn11
I won't reply further to this question about g, i do think i've been clear. and at this point you can be on your merry way still thinking it's wrong. but you simply misunderstood.
n4r9
I've read your paper and followed the arguments and this is where I believe it falls down. Either that or it needs much better explanation.
thelastquestion
I don't think this will happen in the near future, but "ever"? Almost certainly unless humanity stops working on AI systems for some reason. The current approaches to AI have poor reasoning ability. This could possibly be due to a mechanistic flaw or simply be a matter of iteration, i.e., repeatedly trying things and getting feedback about why they are wrong, possibly internally. It's not clear that when we reason, our brains aren't implicitly and explicitly trying all sorts of things and discounting things that seem wrong (lots of neurochemical mechanisms are unclear here). Naive LLM inference isn't doing this, but can iterate within a system; it could be that a proof of a complex theorem requires an extreme version of that kind of iteration. Humans don't tend to spit out nontrivial proofs in one-shot either, so there's currently a significant asymmetry between the amount of human brain computation that goes into a proof of a complex theorem and silicon computation that goes into responding to a prompt.