This resolves "YES" if by the market close date, there is a publically-downloadable full formal proof of Fermat's last theorem in a theorem-proving language such as Coq, Lean, or Isabelle.
Close date updated to 2029-05-01 11:59 pm
Nov 26, 4:21pm: Will we have a formalized proof of Fermat's last theorem by May 2029? → Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
1,000
3.00YES based on this article:
https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/
Correct me if I'm stupid 😂
@BoltonBailey Does this take into account the trajectory of AI assistants? Perhaps it would be more trivial to formalize such a proof later than it is now?
@wadimiusz Hard to say, Kevin is often ready in his writings to admit that neural networks aren't his area of expertise. My take is that if you think AI will be really powerful by 2029 and able to either read papers or make arguments itself, you might think this is likely, but if you were expecting humans to do most of the work, it seems much less likely.
@BoltonBailey In case anyone's wondering why I bet yes. One might see the problem of automatically searching formal proofs for a given theorem as a problem where verifying a suggested candidate is trivial, but proposing a good candidate is damn hard, right? And it makes sense, I guess, to use AIs as good suggestors - even modern LMs, which can generate good ideas sometimes and rubbish at other times; because we already have a nice verifier, we just can't bruteforce all the candidates when the hypothesis space is so huge. That's why I am guessing that finding formalized proofs will be much easier as AI capabilities skyrocket. Let us see in 2029 how off my model is.