Will we have a formalized proof of Fermat's last theorem by 2029-05-01?

Question

This resolves "YES" if by the market close date, there is a publically-downloadable full formal proof of Fermat's last theorem in a theorem-proving language such as Coq, Lean, or Isabelle.

Manifold Markets · Answer

Likely — Manifold Markets prediction market estimates a 69% chance (46 traders, as of Apr 21, 2026).