# Write a program that checks the consistency of modern mathematics

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.