>To preempt the inevitable question in the comments section: yes, we did run these Turing machines for a while, and no, none of them had halted after a day or so. But before you interpret that as evidence in favor of Goldbach, Riemann, and the consistency of ZFC, you should probably know that a Turing machine to test whether all perfect squares are less than 5, produced using Laconic, needed to run for more than an hour before it found the first counterexample (namely, 32=9) and halted. Laconic Turing machines are optimized only for the number of states, not for speed, to put it mildly.

Does anyone know of any speed-optimized tests of ZFC currently running? I'd expect that they're not using Turing machines. . .