4 ms·
Ask HN: Will an AI be able to prove Fermat's last theorem? When?
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?
- bell-cot 2y agoLiterally "ever"? Yes. In a short-term-obsessed online world, where "forever" is just a few years? Probably no.
- zephyrfalcon 2y agoFermat'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 2y agoI 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 2y agohttps://www.techrxiv.org/users/717330/articles/702287-on-fermat-s-last-theorem https://www.techrxiv.org/users/717330/articles/702287-on-fer...
- n4r9 2y agoOn 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 2y agoThis 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 2y agoBut 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 2y agoi 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 2y agoPages 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 2y agoit'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.
- thelastquestion 2y agoI 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.