This market will resolve YES if, before the year 1 0000, a finite proof is discovered, within the standard formulation of Peano Arithmetic, that derives a contradiction (e.g., 0 = 1), and this result is verified and accepted by the mainstream mathematical community. Otherwise, it will resolve NO.