This is a front-end for the Online Encyclopedia of Integer Sequences, made by Christian Perfect. The idea is to provide OEIS entries in non-ancient HTML, and then to think about how they're presented visually. The source code is on GitHub.
%I A369587 #15 Jan 29 2024 19:30:04
%S A369587 2,13,5,5,68,17,44,20,44,9,52,52,31,52,18,31,52,31,10,31,10
%N 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.
%C A369587 See A368946 for the description of the MIU formal system and A369173 for the triangle of corresponding strings.
%C A369587 Strings are encoded by mapping the characters M, I, and U to 3, 1, and 0, respectively.
%C A369587 In case more than one shortest proof exists, the lexicographically earliest one (after encoding) is chosen.
%D A369587 Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.
%H A369587 Wikipedia, <a href="https://en.wikipedia.org/wiki/MU_puzzle">MU Puzzle</a>.
%H A369587 <a href="/index/Go#GEB">Index entries for sequences from "Goedel, Escher, Bach"</a>.
%e A369587 Triangle begins:
%e A369587 [2] 2;
%e A369587 [3] 13 5 5;
%e A369587 [4] 68 17 44 20 44 9;
%e A369587 [5] 52 52 31 52 18 31 52 31 10 31 10;
%e A369587 ...
%e A369587 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.
%t A369587 MIUStrings[n_] := Map["3" <> FromCharacterCode[# + 48] &, Select[Tuples[{0, 1}, n - 1], ! Divisible[Count[#, 1], 3] &]];
%t A369587 MIUNext[s_] := Flatten[{If[StringEndsQ[s, "1"], s <> "0", Nothing], s <> StringDrop[s, 1], StringReplaceList[s, {"111" -> "0", "00" -> ""}]}];
%t A369587 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 *)
%Y A369587 Cf. A368946, A369173, A369411 (analog for "normal" proofs).
%Y A369587 Cf. A024495 (row lengths), A369408 (number of lines), A369586 (proofs).
%K A369587 nonn,tabf,hard,more
%O A369587 2,1
%A A369587 _Paolo Xausa_, Jan 26 2024