@Quillist This market was created Feb 14 2024, but closes Feb 30 2030, which is (more than) 6 years afterwards. Would you mind clarifying the exact date that FLT needs to be formalized by to count for this market?

@BoltonBailey From the title of the post most valid end date would be Feb 14 2029.

I'm going with "yes" based mostly on vague, gut-feeling optimism for improvement in Lean tooling, and the sense that that might lead to a lot more people both wanting to and being more easily able to contribute the necessary (enormous) quantity of work. A more sober consideration of the current facts, however, might indeed lead you to "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.

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 the 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