Will Kevin Buzzard successfully formalize Fermat's Last Theorem in Lean within his 5 year grant?
Basic
11
Ṁ3442030
81%
chance
1D
1W
1M
ALL
Get
1,000
and1.00
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 the Myhill–Nerode theorem be formalized in Lean mathlib by the end of 2024?
89% chance
Will a proof of Fermat's Last Theorem simple enough for Fermat to have possessed be found by 2027?
5% chance
Will Terence Tao write a paper with Lean code in it during the 2026 calendar year?
76% chance
Which theorem prover will have proved the most theorems on Freek's list by end of 2025?
Could Fermat have had a proof of Fermat's Last Theorem?
8% chance