Resolves YES if, before market close, a test case is published that proves 0 = 1 (or similar nonsense) and passes lean4checker.

The test case must use either the latest version of Lean + lean4checker at time of publication, or the version that was available immediately beforehand. (The latter condition allows for the Lean developers fixing a hole as soon as they find it.)

Shenanigans do not count. Shenanigans can include (but are not limited to):

• Redefining core types and operations

• Replacing the lean4checker executable

• Changing the syntax to make a true statement look like a contradiction (e.g. 0 = 1 in the trivial ring)

In the event of an ambiguity, I will try to resolve in the spirit of the market.