Write a program that checks the consistency of modern mathematics

Question

Modern mathematics has been formalised using set theory by various systems of axioms. Zermelo Frankel set theory with the axiom of choice (ZFC) forms an intuitive set of axioms and is hence most popular, though stronger choices exist.

Inspiration: A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory by Adam Yedidia and Scott Aaronson

In this paper, a 7918-state Turing machine has been discovered that "checks" the consistency of ZFC. More specifically, it has been proven impossible to prove the machine as either halting or non-halting within ZFC. Note that if the program actually halts in a finite number of steps, its behaviour is also provably halting in any reasonable axiomatic system since we can enumerate this finite number of steps explicitly. Therefore halting can only mean an inconsistency in ZFC itself.

A 1919-state TM was also discovered subsequently

The method they've used (for the 8000 state machine) is to identify a mathematical statement whose truth has been proven to imply the consistency of ZFC, in this case Friedman's mathematical statement on graphs (section 3.1 of the paper), then written a program in a higher level language to check that, then converted it to a Turing machine

Your task: Write a program in any accepted language on this site (not necessarily a Turing machine) which cannot be proven as halting or non-halting within ZFC. This is code golf, so shortest program wins.

Your program must be deterministic, it cannot use "random" numbers or take external "random" input.

Likely method to go about this would be to identify a mathematical statement which is already known to be independent of ZFC or a stronger system, and check that - though this is by no means the only way to go about it. Here's a list of such statements to get you started.

Related: Analogous challenge for Peano arithmetic

Answer 1

NQL: 335 characters

In The Busy Beaver Frontier page 12, Scott Aaronson mentions that Stefan O'Rear found a 748-state Turing machine that halts iff ZF is inconsistent. Here is the code that compiles to that Turing machine from a higher-level programming language called NQL, based on Laconic. I'm not very familiar with this language, but applying basic golfing techniques yields 397 characters:

global x;global lcm;global l;global num;global denom;global i;global a;global b;global c;global d;proc main(){lcm=1;while(true){x=x+1;l=lcm;while(lcm!=(lcm/l)*l||lcm!=(lcm/x)*x){lcm=lcm+1;}if(x>253){num=0;denom=1;i=1;while(i<=lcm){num=num*i+denom;denom=denom*i;i=i+1;}a=num-denom*x;a=a*a;b=denom*denom;c=0;d=1;i=1;while(i<=x){c=c*i+d;d=d*i;i=i+1;}c=c*c;c=c*c*x;d=d*d;d=d*d;if(a*d>b*c){return;}}}}

I confirmed that the same output is produced as the original program with

diff <(python3 nqlaconic.py --print-tm riemann-matiyasevich-aaronson.nql) \
<(python3 nqlaconic.py --print-tm riemann-matiyasevich-aaronson-golfed.nql)

Applying variable name shortening (this changes the output) yields 335 characters:

global x;global v;global l;global z;global y;global i;global a;global b;global c;global d;proc main(){v=1;while(true){x=x+1;l=v;while(v!=(v/l)*l||v!=(v/x)*x){v=v+1;}if(x>253){z=0;y=1;i=1;while(i<=v){z=z*i+y;y=y*i;i=i+1;}a=z-y*x;a=a*a;b=y*y;c=0;d=1;i=1;while(i<=x){c=c*i+d;d=d*i;i=i+1;}c=c*c;c=c*c*x;d=d*d;d=d*d;if(a*d>b*c){return;}}}}

Given its C-like syntax, I imagine the code could be easily adapted to other languages and shortened further.