Write a program that checks the consistency of modern mathematics
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&gt;253){num=0;denom=1;i=1;while(i&lt;=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&lt;=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&gt;b*c){return;}}}}

I confirmed that the same output is produced as the original program with
diff &lt;(python3 nqlaconic.py --print-tm riemann-matiyasevich-aaronson.nql) \
&lt;(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&gt;253){z=0;y=1;i=1;while(i&lt;=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&lt;=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&gt;b*c){return;}}}}

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