The resolves "YES" if by the market close date, there is a publically-downloadable full formal proof of the modularity theorem (formerly known as the Taniyama-Shimura Conjecture) in a theorem-proving language such as Coq, Lean, or Isabelle.
1,000
3.00Kevin Buzzard, a math professor at Imperial College London, who you must know if you are following Lean and mathlib, announced (2024-01-20) that he was granted a million GBP from UK government to fully formalise Wiles proof of Fermat's Last Theorem in Lean for five years, from 2024-10 to 2029-10. He is preparing a Lean blueprint to share.
https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/
Which is exciting! On the other hand, in terms of this market, it requires Kevin to finish five months earlier to resolve YES.
@SanghyeonSeo His grant isn't really for fully formalizing Wiles proof. The text says:
My proposal is to fully formalise much of the mathematics involved in a modern proof of FLT in the Lean computer proof assistant, thus reducing the (gigantic) task of fully formalising a proof of Fermat's Last Theorem to the task of fully formalising various results from the 1980s. [...] Ultimately the outcomes of the project will be that a computer will be able to understand some proofs from late 20th century mathematics, but also many statements of theorems of 21st century mathematics.
He also wrote in August on Twitter:
I got a research grant to begin the proof of formalising Fermat's Last Theorem in Lean! [...]
The research buys out my teaching and admin for 5 years, which I suspect will not be enough to get it done, but it will certainly be enough to make a big dent in it.
@SanghyeonSeo Another thing to note is that Wiles did not prove the full modularity theorem, only its special case for semistable elliptic curves. Idk how much harder the general case is, but it is probably hard enough not to be a priority for a project focusing on FLT.
@wadimiusz Unclear there is any work on it, or if it could even be formally defined yet.