Will fermats last theorem be formalized in lean down to the axiom in 5 years.

210Ṁ579

2030

49%

chance

ALL

Math

Programming

Get

1,000

to start trading!

People are also trading

Will Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?

56% chance

Which theorems will be formally proven in Lean by the end of 2028?

Will we have a formalized proof of Fermat's last theorem by 2029-05-01?

72% chance

Will we have a formalized proof of Fermat's last theorem by 2049-05-01?

91% chance

When will we have a fully formalized proof of Fermat's Last Theorem?

Will a proof of Fermat's Last Theorem simple enough for Fermat to have possessed be found by 2027?

2% chance

Could Fermat have had a proof of Fermat's Last Theorem?

5% chance

Which theorem prover will have proved the most theorems on Freek's list by end of 2025?

Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?

41% chance

Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?

Sort by:

bought Ṁ5 NO

On a recent talk, Buzzard said "... this is at least a 5 year project - to be frank, it's probably a lot more than 5 years."
Source: https://vimeo.com/969084273

Somewhat unclear resolution - is it sufficient if just the goals of the grant are fulfilled or a full formalization of Fermat down to axioms is required?

@MartinModrak this market resolves yes only if there is a full formalization of Fermat within 5 years.

bought Ṁ50 NO

Worth noting that the goal of the current project is to to formalize FLT assuming any theorems known in the 1980s. If this market only resolves to YES if FLT is formalized all the way to the axioms, then there'd be a bunch more work required than is in-scope in Buzzard's current project.

Still could be possible if that math community rallies around the project, or if AI ends up helping out a lot, but less likely than just Buzzard completing the project he proposed.

@rogs I was unaware of that detail. To maintain the consistency of this market I will remake this one to the claim "Will fermats last theorem be formalized in lean down to the axiom in 5 years" and a new market for just the grant's specs

Apologies for early bettors, luckily this market is 5 years away