cp's OEIS Frontend

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.

A369408 Irregular triangle read by rows: T(n,k) is the length of the shortest proof for the MIU formal system string (theorem) given by A369173(n,k).

This page as a plain text file.
%I A369408 #28 Jan 30 2024 04:11:11
%S A369408 1,4,2,2,11,5,8,5,8,3,9,9,6,9,5,6,9,6,3,6,3
%N A369408 Irregular triangle read by rows: T(n,k) is the length of the shortest proof for the MIU formal system string (theorem) given by A369173(n,k).
%C A369408 See A368946 for the description of the MIU formal system and A369173 for the triangle of the corresponding derivable strings.
%C A369408 The length of the shortest proof for a string (theorem) S is the number of lines of the shortest possible derivation of S.
%C A369408 A369173(n,k) first appears in row T(n,k) - 1 in triangle A368946.
%D A369408 Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.
%H A369408 Wikipedia, <a href="https://en.wikipedia.org/wiki/MU_puzzle">MU Puzzle</a>.
%H A369408 <a href="/index/Go#GEB">Index entries for sequences from "Goedel, Escher, Bach"</a>.
%F A369408 T(n,k) <= A369410(n,k).
%e A369408 Triangle begins:
%e A369408   [2]  1;
%e A369408   [3]  4  2  2;
%e A369408   [4] 11  5  8  5  8  3;
%e A369408   [5]  9  9  6  9  5  6  9  6  3  6  3;
%e A369408   ...
%e A369408 For the theorem MUI (301), which is given by A369173(3,1), the shortest derivation from the axiom MI is MI (31) -> MII (311) -> MIIII (31111) -> MIU (301) (4 lines), so T(3,1) = 4.
%t A369408 MIUStringsW3[n_] := Map[FromCharacterCode[# + 48]&, Select[Tuples[{0, 1}, n - 1], ! Divisible[Count[#, 1], 3] &]];
%t A369408 MIUStepDW3[s_] := DeleteDuplicates[Flatten[Map[{If[StringEndsQ[#, "1"], # <> "0", Nothing], # <> #, StringReplaceList[#, {"111" -> "0", "00" -> ""}]} &, s]]];
%t A369408 Module[{rowmax = 5, treedepth = 10, tree}, tree = NestList[MIUStepDW3, {"1"}, treedepth]; Map[Quiet[Check[Position[tree, #, {2}][[1,1]], "Not found"]]&, Array[MIUStringsW3, rowmax - 1, 2], {2}]]
%Y A369408 Cf. A024495 (row lengths), A331536, A368946, A369173, A369410.
%Y A369408 Cf. A369586 (proofs), A369587 (number of symbols).
%K A369408 nonn,tabf,hard,more
%O A369408 2,2
%A A369408 _Paolo Xausa_, Jan 22 2024