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

https://news.ycombinator.com/item?id=40499443

by logicallee • 2 years ago

2 16 2 years ago

news.ycombinator.com

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• 2 years ago

Literally "ever"? Yes.

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

zephyrfalcon• 2 years ago

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• 2 years ago

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.

levn116• 2 years ago

https://www.techrxiv.org/users/717330/articles/702287-on-fer...

n4r96• 2 years ago

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.

levn116• 2 years ago

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.

thelastquestion• 2 years ago

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.

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

Related Stories