experimental - introduce Hadwiger-Nelson problem as ~ undiscolmin

[ProgramCrafter]

I present an approach to formalizing conjectures, with syntax checks included and status clearly described: include the relevant hypotheses, and reprove them with ~idi. I have no strong opinion on whether it will fit the database.

[ProgramCrafter]

relevant to #4994

[tirix]

I think in the past we have simply added conjectures or unattainable theorems as axioms, see for example ax-tgoldbachgt, or ax-ros335. Maybe the same could be done here?

The axioms can be marked as "New Usage Discouraged" in order to notice when it is used, and we also have the tools to find if a given theorem uses a given axiom.

Tools like metamath-knife and MMJ2 can check that the statements are syntactically correct.

Naturally I would also find it OK to include in set.mm this kind of axioms, and theorems derived from them. Until now I think we have kept them in mathboxes, but there could be a section in main with theories based on unproven statements.

[ProgramCrafter]

Hypotheses are IMO more convenient in that

1. they do not need a soundness check (the worst is, they will be unsatisfiable),
2. so a hypothesis' "definition" of a term can even be self-referential (or a set of equations which is not strictly a definition),
3. so less review is needed when a whole list of conjectures gets formalized (which is the content of Translating Deepmind's formal conjecture collection to Metamath? #4994),
4. syntax checking is supported by all verifiers (I happen to use metamath-exe currently so having the check there is convenient),
5. the syntax proof is explicitly written down.

And having more axioms would also clutter my axiom-usage-viewing UI 😀

[ProgramCrafter]

It crossed my mind that I should also list benefits of axioms:

• they can be replaced with their proofs transparently, with no changes to upstream theorems (except $j statements, which shouldn't include that axiom anymore)
• an axiom is all-substitutions, i.e. its usage can substitute anything, while a hypothesis is fixed
• no ~idi trickery with repeated steps means better support in mmj2, mmt1 and other .mmp-based editors