Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
Basic
34
4.4k
2029
63%
chance
[tweet]

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?

Get Ṁ600 play money
Sort by:
predicts NO

Most of the work in formalization is domain modeling and API design. Given the wide range of concepts that Wiles' proof depends on, I doubt that such a project will be done any time soon.

In a discussion on the Lean forum, Kevin Buzzard seemed pretty pessimistic. Seeing as he would probably be best suited to know the challenges of formalizing FLT, I'm adjusting downward.

predicts YES

@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?

predicts NO

@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.

predicts YES

@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.

See https://github.com/leanprover-community/flt-regular for a project to formalize a special case.
Amazing if there is, so much groundwork to get to that. I'll chuck M$1 into this black hole for some 2029 hawking radiation.