Will we have a formalized proof of Fermat's last theorem by May 2029?
May 2, 2032
M$14 bet
The 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.

Bolton Bailey 22 days ago

See https://github.com/leanprover-community/flt-regular for a project to formalize a special case.

Undox bought M$1 of NO23 days ago

Amazing if there is, so much groundwork to get to that. I'll chuck M$1 into this black hole for some 2029 hawking radiation.