Resolution criteria
The market resolves YES if a complete formalization of Fermat's Last Theorem (the full statement: for all integers n ≥ 3, the equation x^n + y^n = z^n has no positive integer solutions) is merged into Lean's Mathlib library by December 31, 2026. Resolution is based on the official Lean Mathlib repository at https://github.com/leanprover-community/mathlib4. The formalization must cover the entire theorem as originally proved by Wiles and Taylor, not just special cases like the regular prime case.
1,000I am not super familiar with how merging into the Mathlib library works. Is there a scenario where the formalization exists, everyone agrees that it is correct, but it is not merged? Either because there is some process that takes time or because it is deemed too "long" or something to be part of Mathlib?
Have the other bigger Lean formalization projects ended up merged into Mathlib? I thought it was more of a toolset to do math, not the repository of all results formalized (these two things overlap, but not completely?)