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.
Update 2026-01-27 (PST) (AI summary of creator comment): The creator has confirmed they will not change the resolution criteria despite acknowledging a potential mismatch between what the market intends to measure (existence of a finished formalization) versus what it actually measures (whether it's merged into Mathlib). The market will continue to resolve based on the Mathlib merge requirement as originally stated.
1,000People are also trading
I 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?)
@rayman2000 Oh this scenario is almost certainly what will happen, at least initially. My FLT repo https://github.com/ImperialCollegeLondon/FLT (which is AFAIK the only repo actively working on FLT) is downstream from mathilb, and upstreaming happens more slowly (the code quality of mathlib is a bit higher than the code quality in the FLT repo because I'm a bit less fussy about what makes it into FLT than the mathlib maintainers).
In both FLT and other formalization project, a common endgame after the theorem is proved is that many basic facts which were used end up in mathlib, but the main theorem does not. For example there is plenty of upstreaming happening from Floris van Doorn's Carleson project, but my impression is that the main theorem might well not make it into mathlib itself, or perhaps more precisely that nobody is currently working, or has plans to work on, getting the main theorem into mathlib.
@KevinBuzzard Thanks for the explanation!
@Grothenfla Then it seems like there is a mismatch between what this market wants to measure (is there a finished formalization) and what is actually measured (how mathlib merges things)
@rayman2000 Yeah, you're right. I will not change the criteria to not harm the people who already bet. Maybe I will create another bet soon. @KevinBuzzard Thank you for the clarification!