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?
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.
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.
Literally "ever"? Yes.
In a short-term-obsessed online world, where "forever" is just a few years? Probably no.
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.