Will Kevin Buzzard successfully formalize Fermat's Last Theorem in Lean within his 5 year grant?
Mini
11
Ṁ3442030
81%
chance
1D
1W
1M
ALL
Get Ṁ1,000 play money
Sort by:
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
@MartinModrak this market resolves yes only if there is a full formalization of Fermat within 5 years.
Related questions
Related questions
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
62% chance
When will we have a fully formalized proof of Fermat's Last Theorem?
Will Fermat's last theorem be formalized before AI gets IMO gold?
23% chance
Will we have a formalized proof of Fermat's last theorem by 2049-05-01?
89% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
40% chance
Will a proof of Fermat's Last Theorem simple enough for Fermat to have possessed be found by 2027?
5% chance
Could Fermat have had a proof of Fermat's Last Theorem?
8% chance
Will Terence Tao write a paper with Lean code in it during the 2026 calendar year?
74% chance
Which theorem prover will have proved the most theorems on Freek's list by end of 2025?
Will the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?
89% chance