Will we have a formalized proof of the Modularity theorem by 2029-05-01?
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
28
1kṀ7834
2029
65%
chance

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.

Get
Ṁ1,000
to start trading!


Sort by:
predictedYES 1y

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

predictedNO

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

predictedNO

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

2y

How far is mathlib today?

predictedYES 2y

@wadimiusz Unclear there is any work on it, or if it could even be formally defined yet.

What is this?

What is Manifold?
Manifold is the world's largest social prediction market.
Get accurate real-time odds on politics, tech, sports, and more.
Or create your own play-money betting market on any question you care about.
Are our predictions accurate?
Yes! Manifold is very well calibrated, with forecasts on average within 4 percentage points of the true probability. Our probabilities are created by users buying and selling shares of a market.
In the 2022 US midterm elections, we outperformed all other prediction market platforms and were in line with FiveThirtyEight’s performance. Many people who don't like betting still use Manifold to get reliable news.
ṀWhy use play money?
Mana (Ṁ) is the play-money currency used to bet on Manifold. It cannot be converted to cash. All users start with Ṁ1,000 for free.
Play money means it's much easier for anyone anywhere in the world to get started and try out forecasting without any risk. It also means there's more freedom to create and bet on any type of question.
© Manifold Markets, Inc.Terms + Mana-only TermsPrivacyRules