A369587 Irregular triangle read by rows: row n lists the number of symbols of the shortest proof (see comments) for each of the distinct derivable strings (theorems) in the MIU formal system that are n characters long.

2, 13, 5, 5, 68, 17, 44, 20, 44, 9, 52, 52, 31, 52, 18, 31, 52, 31, 10, 31, 10

Offset: 2

Author

Paolo Xausa, Jan 26 2024

Keywords

• nonn
• tabf
• hard
• more

Comments

See A368946 for the description of the MIU formal system and A369173 for the triangle of corresponding strings.

Strings are encoded by mapping the characters M, I, and U to 3, 1, and 0, respectively.

In case more than one shortest proof exists, the lexicographically earliest one (after encoding) is chosen.

Examples

			Triangle begins:
  [2]  2;
  [3] 13  5  5;
  [4] 68 17 44 20 44  9;
  [5] 52 52 31 52 18 31 52 31 10 31 10;
  ...
For the theorem MIUU (3100), which is given by A369173(4,4), the shortest proof is MI (31) -> MII (311) -> MIIII (31111) -> MIIIIU (311110) -> MIUU (3100), which consists of a total of 20 symbols (counting only M, I and U characters): T(4,4) is therefore 20.
		

References

• Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.

Links

• Wikipedia, MU Puzzle.
• Index entries for sequences from "Goedel, Escher, Bach".

Crossrefs

Cf. A368946, A369173, A369411 (analog for "normal" proofs).

Cf. A024495 (row lengths), A369408 (number of lines), A369586 (proofs).

Programs

Mathematica

MIUStrings[n_] := Map["3" <> FromCharacterCode[# + 48] &, Select[Tuples[{0, 1}, n - 1], ! Divisible[Count[#, 1], 3] &]];
MIUNext[s_] := Flatten[{If[StringEndsQ[s, "1"], s <> "0", Nothing], s <> StringDrop[s, 1], StringReplaceList[s, {"111" -> "0", "00" -> ""}]}];
Module[{uptolen = 5, searchdepth = 10, mi = "31", g}, g = NestGraph[MIUNext, mi, searchdepth]; Map[Quiet[Check[Map[FromDigits, StringLength[StringJoin[If[# == mi, #, First[Sort[FindPath[g, mi, #, {GraphDistance[g, mi, #]}, All]]]]]]], "Not found"]] &, Array[MIUStrings, uptolen - 1, 2], {2}]] (* Considers theorems up to 5 characters long, looking up to 10 steps away from the MI axiom -- please note it takes a while *)