cp's OEIS Frontend

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).

%I A369586 #18 Jan 31 2024 04:03:23
%S A369586 31,31,311,31111,301,31,310,31,311,31,311,31111,311111111,3011111,
%T A369586 30011,300110011,3001100110,30011110,300100,3001,31,311,31111,301,
%U A369586 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
%N 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).
%C A369586 See A368946 for the description of the MIU formal system.
%C A369586 Strings are encoded by mapping the characters M, I, and U to 3, 1, and 0, respectively.
%C A369586 In case more than one shortest proof exists, the lexicographically earliest one (after encoding) is chosen.
%D A369586 Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.
%H A369586 Paolo Xausa, <a href="/A369586/b369586.txt">Table of n, a(n) for n = 1..120</a> (rows 1..21 of the triangle, flattened).
%H A369586 Wikipedia, <a href="https://en.wikipedia.org/wiki/MU_puzzle">MU Puzzle</a>.
%H A369586 <a href="/index/Go#GEB">Index entries for sequences from "Goedel, Escher, Bach"</a>.
%e A369586 Triangle begins:
%e A369586   [1] 31;
%e A369586   [2] 31 311 31111 301;
%e A369586   [3] 31 310;
%e A369586   [4] 31 311;
%e A369586   [5] 31 311 31111 ... 30011 300110011 3001100110 30011110 300100 3001;
%e A369586   ...
%e A369586 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).
%e A369586 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).
%t A369586 MIUStrings[n_] := Map["3" <> FromCharacterCode[# + 48] &, Select[Tuples[{0, 1}, n - 1], ! Divisible[Count[#, 1], 3] &]];
%t A369586 MIUNext[s_] := Flatten[{If[StringEndsQ[s, "1"], s <> "0", Nothing], s <> StringDrop[s, 1], StringReplaceList[s, {"111" -> "0", "00" -> ""}]}];
%t A369586 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 *)
%Y A369586 Cf. A368946, A369173, A369409 (analog for "normal" proofs).
%Y A369586 Cf. A369408 (row lengths), A369587 (number of symbols).
%K A369586 nonn,tabf
%O A369586 1,1
%A A369586 _Paolo Xausa_, Jan 26 2024