FOM: chess "theorems"

[Harvey Friedman]

>...These professionals are capable of showing
>how these conjectures can be turned into chess theorems just
>actually playing the proper moves against any defense chosen.

The chess professionals are not turning these conjectures into chess
theorems merely by playing (even absolutely) correct moves against
particular defenses, unless you mean something unusual by "chess theorems."

I conjecture that "the original chess position is a draw" is not decidable
in ZFC using at most 2^100 symbols, even if ZFC is augmented in standard
ways to support abbreviations (which is required in order to make ZFC
capable of actual formalization).