A369586 Irregular triangle read by rows: row n lists the lines of the shortest proof for the MIU formal system string (theorem) given by A369173(n+1).

31, 31, 311, 31111, 301, 31, 310, 31, 311, 31, 311, 31111, 311111111, 3011111, 30011, 300110011, 3001100110, 30011110, 300100, 3001, 31, 311, 31111, 301, 3010, 31, 311, 31111, 311111111, 3011111, 30111110, 301100, 3011, 31, 311, 31111, 311110, 3100, 31, 311, 31111, 311111111, 3101111, 31011110, 310100, 3101, 31, 311, 3110

Offset: 1

Author

Paolo Xausa, Jan 26 2024

Keywords

• nonn
• tabf

Comments

See A368946 for the description of the MIU formal system.

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:
  [1] 31;
  [2] 31 311 31111 301;
  [3] 31 310;
  [4] 31 311;
  [5] 31 311 31111 ... 30011 300110011 3001100110 30011110 300100 3001;
  ...
For the theorem MUI (301), which is given by A369173(3,1) or (after flattening) A369173(3), the shortest proof is 31 -> 311 -> 31111 -> 301, which is row 2 of the present sequence (same as the "normal" proof, cf. A369409).
For the theorem MIUU (3100), which is given by A369173(4,4) or (after flattening) A369173(9), the shortest proof is 31 -> 311 -> 31111 -> 311110 -> 3100, which is row 8 of the present sequence (shorter than the "normal" proof).
		

References

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

Links

• Paolo Xausa, Table of n, a(n) for n = 1..120 (rows 1..21 of the triangle, flattened).
• Wikipedia, MU Puzzle.
• Index entries for sequences from "Goedel, Escher, Bach".

Crossrefs

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

Cf. A369408 (row lengths), A369587 (number of symbols).

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, If[# == mi, {#}, First[Sort[FindPath[g, mi, #, {GraphDistance[g, mi, #]}, All]]]]], {"Not found"}]] &, Flatten[Array[MIUStrings, uptolen - 1, 2]]]] (* Considers theorems up to 5 characters long, looking up to 10 steps away from the MI axiom -- please note it takes a while *)