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.

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

@Quillist