login
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).
6
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,1
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.
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.
EXAMPLE
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).
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 *)
CROSSREFS
Cf. A368946, A369173, A369409 (analog for "normal" proofs).
Cf. A369408 (row lengths), A369587 (number of symbols).
Sequence in context: A040931 A022365 A070921 * A369409 A165852 A291523
KEYWORD
nonn,tabf
AUTHOR
Paolo Xausa, Jan 26 2024
STATUS
approved