login
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.
5
2, 13, 5, 5, 68, 17, 44, 20, 44, 9, 52, 52, 31, 52, 18, 31, 52, 31, 10, 31, 10
OFFSET
2,1
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.
REFERENCES
Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.
EXAMPLE
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.
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 *)
CROSSREFS
Cf. A368946, A369173, A369411 (analog for "normal" proofs).
Cf. A024495 (row lengths), A369408 (number of lines), A369586 (proofs).
Sequence in context: A335817 A093079 A095417 * A366719 A129733 A084160
KEYWORD
nonn,tabf,hard,more
AUTHOR
Paolo Xausa, Jan 26 2024
STATUS
approved